let A be real-membered set ; :: thesis: for x being real number
for y being Real holds
( y in x ++ A iff ex z being Real st
( z in A & y = x + z ) )
let x be real number ; :: thesis: for y being Real holds
( y in x ++ A iff ex z being Real st
( z in A & y = x + z ) )
let 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 Element of REAL st
( w in A & y = x + w )
then consider w being Element of COMPLEX such that
A1: ( y = x + w & w in A ) by MEMBER_1:143;
A c= REAL by MEMBERED:3;
then reconsider w = w as Element of 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