:: deftheorem Def2 defines the_perpendicular_bisector EUCLID12:def 4 :

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

for b_{3} being Element of line_of_REAL 2 holds

( b_{3} = the_perpendicular_bisector (A,B) iff ex L1, L2 being Element of line_of_REAL 2 st

( b_{3} = L2 & L1 = Line (A,B) & L1 _|_ L2 & L1 /\ L2 = {(the_midpoint_of_the_segment (A,B))} ) );

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

for b

( b

( b