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