let A1, A2 be Subset of REAL ; :: thesis: ( ( for y being Real holds
( y in A1 iff ex z being Real st
( z in A & y = x + z ) ) ) & ( for y being Real holds
( y in A2 iff ex z being Real st
( z in A & y = x + z ) ) ) implies A1 = A2 )
assume that
A1: for y being Real holds
( y in A1 iff ex z being Real st
( z in A & y = x + z ) ) and
A2: for y being Real holds
( y in A2 iff ex z being Real st
( z in A & y = x + z ) ) ; :: thesis: A1 = A2
thus A1 c= A2 :: according to XBOOLE_0:def 10 :: thesis: A2 c= A1

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in A1 or y in A2 )
assume A3: y in A1 ; :: thesis: y in A2
then reconsider y = y as Real ;
ex z being Real st
( z in A & y = x + z ) by A1, A3;
hence y in A2 by A2; :: thesis: verum

end;

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in A2 or y in A1 )
assume A4: y in A2 ; :: thesis: y in A1
then reconsider y = y as Real ;
ex z being Real st
( z in A & y = x + z ) by A2, A4;
hence y in A1 by A1; :: thesis: verum