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