let n be Nat; :: thesis: n in n + 1
reconsider n = n as Element of NAT by ORDINAL1:def 12;
n < n + 1 by XREAL_1:29;
then n in { l where l is Element of NAT : l < n + 1 } ;
hence n in n + 1 by AXIOMS:4; :: thesis: verum