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 )
A2: ( - z in REAL or - z in {-infty,+infty} ) by XBOOLE_0:def 3;
assume z in REAL ; :: thesis: - z in REAL
hence - z in REAL by A2, TARSKI:def 2; :: 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