reconsider p' = p as Element of REAL n ;
- p' is Point of (TOP-REAL n) ;
hence - p is Point of (TOP-REAL n) ; :: thesis: verum