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