let A, B be Point of (TOP-REAL 2); :: thesis: ( A <> B implies the_perpendicular_bisector (A,B) is being_line )
assume A <> B ; :: thesis: the_perpendicular_bisector (A,B) is being_line
then consider L1, L2 being Element of line_of_REAL 2 such that
A1: the_perpendicular_bisector (A,B) = L2 and
L1 = Line (A,B) and
A2: L1 _|_ L2 and
L1 /\ L2 = {(the_midpoint_of_the_segment (A,B))} by Def2;
thus the_perpendicular_bisector (A,B) is being_line by A1, A2, EUCLIDLP:67; :: thesis: verum