let x be ext-real number ; :: 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 number ;
- 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 number ;
- a is real ;
hence - x in REAL by XREAL_0:def 1; :: thesis: verum