theorem Th44: :: EUCLID12:59

for A, B being Point of (TOP-REAL 2)
for L1, L2 being Element of line_of_REAL 2 st A <> B & L1 = Line (A,B) & L1 _|_ L2 & the_midpoint_of_the_segment (A,B) in L2 holds
L2 = the_perpendicular_bisector (A,B)