p + (- r) is Point of (TOP-REAL n) ;
hence p - r is Point of (TOP-REAL n) ; :: thesis: verum