let x be ExtReal; :: thesis: ( - x in REAL iff x in REAL )
hereby :: thesis: ( x in REAL implies - x in REAL )
assume - x in REAL ; :: thesis: x in REAL
then reconsider a = - x as Real ;
- a in REAL by XREAL_0:def 1;
hence x in REAL ; :: thesis: verum
end;
assume x in REAL ; :: thesis: - x in REAL
then reconsider a = x as Real ;
- a is real ;
hence - x in REAL by XREAL_0:def 1; :: thesis: verum