let q1, q, q2 be Point of (TOP-REAL 2); :: thesis: dist ((q1 - q),(q2 - q)) = dist (q1,q2)
( q1 - q = q1 + (- q) & q2 - q = q2 + (- q) ) by EUCLID:45;
hence dist ((q1 - q),(q2 - q)) = dist (q1,q2) by Th21; :: thesis: verum