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 RLVECT_1:33;
hence dist ((q - q1),(q - q2)) = dist ((q1 - q),(q2 - q)) by Th24
.= dist (q1,q2) by Th23 ;
:: thesis: verum