let A be real-membered set ; :: thesis: for x, y being Real holds
( y in x ++ A iff ex z being Real st
( z in A & y = x + z ) )
let x, y be Real; :: thesis: ( y in x ++ A iff ex z being Real st
( z in A & y = x + z ) )

hereby :: thesis: ( ex z being Real st
( z in A & y = x + z ) implies y in x ++ A )

assume y in x ++ A ; :: thesis: ex w being Real st
( w in A & y = x + w )
then consider w being Complex such that
A1: ( y = x + w & w in A ) by MEMBER_1:143;
reconsider w = w as Real by A1;
take w = w; :: thesis: ( w in A & y = x + w )
thus ( w in A & y = x + w ) by A1; :: thesis: verum

end;

given z being Real such that A2: ( z in A & y = x + z ) ; :: thesis: y in x ++ A
thus y in x ++ A by A2, MEMBER_1:141; :: thesis: verum