theorem Th25: :: JORDAN1K:25

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