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