let A, B be Point of (TOP-REAL 2); :: thesis: ( A <> B implies the_midpoint_of_the_segment (A,B) in the_perpendicular_bisector (A,B) )

assume A <> B ; :: thesis: 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; :: thesis: verum

assume A <> B ; :: thesis: 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; :: thesis: verum