let q, q1, q2 be Point of (TOP-REAL 2); :: thesis: dist (q - q1),(q - q2) = dist q1,q2
( - (q - q1) = q1 - q & - (q - q2) = q2 - q ) by EUCLID:48;
hence dist (q - q1),(q - q2) = dist (q1 - q),(q2 - q) by Th24
.= dist q1,q2 by Th23 ;
:: thesis: verum