let Z1, Z2 be Subset of ExtREAL ; :: thesis: ( ( for z being R_eal holds
( z in Z1 iff ex x being R_eal st
( x in X & z = - x ) ) ) & ( for z being R_eal holds
( z in Z2 iff ex x being R_eal st
( x in X & z = - x ) ) ) implies Z1 = Z2 )
assume that
A2: for z being R_eal holds
( z in Z1 iff ex x being R_eal st
( x in X & z = - x ) ) and
A3: for z being R_eal holds
( z in Z2 iff ex x being R_eal st
( x in X & z = - x ) ) ; :: thesis: Z1 = Z2
for z being set holds
( z in Z1 iff z in Z2 )

proof

let z be set ; :: thesis: ( z in Z1 iff z in Z2 )
thus ( z in Z1 implies z in Z2 ) :: thesis: ( z in Z2 implies z in Z1 )

proof

assume A4: z in Z1 ; :: thesis: z in Z2
then reconsider z = z as R_eal ;
ex x being R_eal st
( x in X & z = - x ) by A2, A4;
hence z in Z2 by A3; :: thesis: verum

end;

assume A5: z in Z2 ; :: thesis: z in Z1
then reconsider z = z as R_eal ;
ex x being R_eal st
( x in X & z = - x ) by A3, A5;
hence z in Z1 by A2; :: thesis: verum

end;

hence Z1 = Z2 by TARSKI:2; :: thesis: verum