let h, i, j be Nat; :: thesis: ( i <= j implies i * h <= j * h )
0 <= h by Th2;
hence ( i <= j implies i * h <= j * h ) by XREAL_1:64; :: thesis: verum