theorem Th43: :: EUCLID12:58

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