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