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

A1: for z being R_eal st z in REAL holds

- z in REAL

proof

( - z in REAL implies z in REAL )
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;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

proof

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

then - (- z) in REAL by A1;

hence z in REAL ; :: thesis: verum

end;then - (- z) in REAL by A1;

hence z in REAL ; :: thesis: verum