let A be Subset of REAL; :: thesis: ( 0 in A & ( for x being Real st x in A holds
x + 1 in A ) implies for n being Nat holds n in A )
assume A1: 0 in A ; :: thesis: ( ex x being Real st
( x in A & not x + 1 in A ) or for n being Nat holds n in A )
assume for x being Real st x in A holds
x + 1 in A ; :: thesis: for n being Nat holds n in A
then for x being real number st x in A holds
x + 1 in A ;
then A2: NAT c= A by A1, AXIOMS:29;
let n be Nat; :: thesis: n in A
n in NAT by ORDINAL1:def 13;
hence n in A by A2; :: thesis: verum