let X be non empty Subset of ExtREAL ; :: thesis: - (- X) = X
for z being R_eal holds
( z in X iff ex x being R_eal st
( x in - X & z = - x ) )

proof

let z be R_eal; :: thesis: ( z in X iff ex x being R_eal st
( x in - X & z = - x ) )
thus ( z in X implies ex x being R_eal st
( x in - X & z = - x ) ) :: thesis: ( ex x being R_eal st
( x in - X & z = - x ) implies z in X )

proof

assume A1: z in X ; :: thesis: ex x being R_eal st
( x in - X & z = - x )
set x = - z;
A2: z = - (- z) ;
- z in - X by A1, Def6;
hence ex x being R_eal st
( x in - X & z = - x ) by A2; :: thesis: verum

end;

given x being R_eal such that A3: ( x in - X & z = - x ) ; :: thesis: z in X
ex a being R_eal st
( a in X & x = - a ) by A3, Def6;
hence z in X by A3; :: thesis: verum

end;

hence - (- X) = X by Def6; :: thesis: verum