theorem :: EUCLID12:53

for A, B being Point of (TOP-REAL 2) st A <> B holds
the_perpendicular_bisector (A,B) is being_line