theorem Th41: :: EUCLID12:56

for A, B, C being Point of (TOP-REAL 2) st A <> B & C in the_perpendicular_bisector (A,B) holds
|.(C - A).| = |.(C - B).|