let z be R_eal; :: thesis: ( z in REAL iff - z in REAL )
A1: for z being R_eal st z in REAL holds
- z in REAL

proof

let z be R_eal; :: thesis: ( z in REAL implies - z in REAL )
assume A2: z in REAL ; :: thesis: - z in REAL
( - z in REAL or - z in {-infty ,+infty } ) by XBOOLE_0:def 3;
then ( - z in REAL or - z = -infty or - z = +infty ) by TARSKI:def 2;
then ( - z in REAL or - (- z) = +infty or - (- z) = -infty ) by XXREAL_3:def 3;
hence - z in REAL by A2; :: thesis: verum

end;

( - z in REAL implies z in REAL )

proof

assume - z in REAL ; :: thesis: z in REAL
then - (- z) in REAL by A1;
hence z in REAL ; :: thesis: verum

end;

hence ( z in REAL iff - z in REAL ) by A1; :: thesis: verum