theorem :: EUCLID12:54

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