:: deftheorem Def2 defines the_perpendicular_bisector EUCLID12:def 4 :
for A, B being Element of (TOP-REAL 2) st A <> B holds
for b₃ being Element of line_of_REAL 2 holds
( b₃ = the_perpendicular_bisector (A,B) iff ex L1, L2 being Element of line_of_REAL 2 st
( b₃ = L2 & L1 = Line (A,B) & L1 _|_ L2 & L1 /\ L2 = {(the_midpoint_of_the_segment (A,B))} ) );