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