theorem Th23: :: JORDAN1K:23

for q, q1, q2 being Point of (TOP-REAL 2) holds dist ((q1 - q),(q2 - q)) = dist (q1,q2) by Th21;