theorem Th45: :: EUCLID12:60

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