∀ n1 n2 m1 m2, n1 ≤ n2 ⇒ m1 ≤ m2 ⇒ (n1 × m1) ≤ (n2 × m2)

Theorem le_times : forall (n1:nat), forall (n2:nat), forall (m1:nat), forall (m2:nat), (le n1 n2) -> (le m1 m2) -> le (times n1 m1) (times n2 m2).

theorem le_times : \forall (n1:nat). \forall (n2:nat). \forall (m1:nat). \forall (m2:nat). ((le) n1 n2) -> ((le) m1 m2) -> (le) ((times) n1 m1) ((times) n2 m2).

theorem le_times : forall (n1:nat.nat) , forall (n2:nat.nat) , forall (m1:nat.nat) , forall (m2:nat.nat) , ((((nat.le_) ) (n1)) (n2)) -> ((((nat.le_) ) (m1)) (m2)) -> (((nat.le_) ) ((((nat.times) ) (n1)) (m1))) ((((nat.times) ) (n2)) (m2)).

le_times : LEMMA (FORALL(n1:nat_sttfa.sttfa_nat):(FORALL(n2:nat_sttfa.sttfa_nat):(FORALL(m1:nat_sttfa.sttfa_nat):(FORALL(m2:nat_sttfa.sttfa_nat):(nat_sttfa.le(n1)(n2) => (nat_sttfa.le(m1)(m2) => nat_sttfa.le(nat_sttfa.times(n1)(m1))(nat_sttfa.times(n2)(m2))))))))

Printing for OpenTheory is not working at the moment.