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)

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)