let i be natural Number ; :: thesis: 0 < i + 1
0 <= i by Th2;
hence 0 < i + 1 ; :: thesis: verum