let X be non empty Subset of ExtREAL ; :: thesis: for z being R_eal holds
( z in X iff - z in - X )
let z be R_eal; :: thesis: ( z in X iff - z in - X )
( - z in - X implies z in X )

proof

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

end;

hence ( z in X iff - z in - X ) by Def6; :: thesis: verum