let i, j, h be Nat; :: thesis: ( i <= j implies i <= j + h )
assume A1: i <= j ; :: thesis: i <= j + h
0 <= h by Th2;
then ( i + 0 <= i + h & i + h <= j + h & i + 0 = i ) by A1, XREAL_1:9;
hence i <= j + h by XXREAL_0:2; :: thesis: verum