let i be Nat; :: thesis: 0 < i + 1
assume A1: 0 >= i + 1 ; :: thesis: contradiction
0 <= i by Th2;
hence contradiction by A1; :: thesis: verum