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