let A be Subset of REAL; :: thesis:
assume that
A1: 0 in A and
A2: for x being Real st x in A holds
x + 1 in A ; :: thesis:
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

let x9, y9 be Element of REAL+ ; :: thesis:
assume that
A5: x9 in B and
A6: y9 = 1 ; :: thesis:
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:

end;