let a1, b1, c1, a2, b2, c2 be Nat; :: thesis: ( a1 <= a2 & b1 <= b2 & c1 <= c2 implies (a1 * b1) * c1 <= (a2 * b2) * c2 )
assume ( a1 <= a2 & b1 <= b2 ) ; :: thesis: ( not c1 <= c2 or (a1 * b1) * c1 <= (a2 * b2) * c2 )
then a1 * b1 <= a2 * b2 by XREAL_1:66;
hence ( not c1 <= c2 or (a1 * b1) * c1 <= (a2 * b2) * c2 ) by XREAL_1:66; :: thesis: verum