let i, j, h be natural Number ; :: 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