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

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

end;

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

end;

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