let n be Element of NAT ; :: thesis: n in n + 1
n < n + 1 by NAT_1:13;
then n in { k where k is Element of NAT : k < n + 1 } ;
hence n in n + 1 by AXIOMS:30; :: thesis: verum