let i, j be natural Number ; :: thesis: i <= i + j
( 0 + i = i & 0 <= j ) by Th2;
hence i <= i + j by XREAL_1:7; :: thesis: verum