let A be Subset of REAL; :: thesis: ( 0 in A & ( for x being Real st x in A holds
x + 1 in A ) implies NAT c= A )
assume that
A1: 0 in A and
A2: for x being Real st x in A holds
x + 1 in A ; :: thesis: NAT c= A
reconsider B = A /\ REAL+ as Subset of REAL+ by XBOOLE_1:17;
A3: B c= A by XBOOLE_1:17;
A4: for x9, y9 being Element of REAL+ st x9 in B & y9 = 1 holds
x9 + y9 in B

proof

let x9, y9 be Element of REAL+ ; :: thesis: ( x9 in B & y9 = 1 implies x9 + y9 in B )
assume that
A5: x9 in B and
A6: y9 = 1 ; :: thesis: x9 + y9 in B
reconsider x = x9 as Element of REAL by ARYTM_0:1;
reconsider y = 1 as Element of REAL by NUMBERS:19;
reconsider xx = x as Real ;
xx + 1 in A by A2, A3, A5;
then ( ex x99, y99 being Element of REAL+ st
( x = x99 & 1 = y99 & + (x,y) = x99 + y99 ) & + (x,y) in A ) by Lm3, ARYTM_0:def 1, ARYTM_2:20;
hence x9 + y9 in B by A6, XBOOLE_0:def 4; :: thesis: verum

end;

0 in B by A1, ARYTM_2:20, XBOOLE_0:def 4;
then NAT c= B by A4, ARYTM_2:17;
hence NAT c= A by A3; :: thesis: verum