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 NAT c= A by A1, AXIOMS:3;
hence for n being Nat holds n in A by ORDINAL1:def 12; :: thesis: verum