let A, B be Point of (TOP-REAL 2); ( A <> B implies the_midpoint_of_the_segment (A,B) in the_perpendicular_bisector (A,B) )
assume
A <> B
; the_midpoint_of_the_segment (A,B) in the_perpendicular_bisector (A,B)
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) & L1 _|_ L2 )
and
A2:
L1 /\ L2 = {(the_midpoint_of_the_segment (A,B))}
by Def2;
the_midpoint_of_the_segment (A,B) in L1 /\ L2
by A2, TARSKI:def 1;
hence
the_midpoint_of_the_segment (A,B) in the_perpendicular_bisector (A,B)
by A1, XBOOLE_0:def 4; verum