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