let A, B be Point of (TOP-REAL 2); :: thesis: for L1, L2 being Element of line_of_REAL 2 st A <> B & L1 = Line (A,B) & L1 _|_ L2 & the_midpoint_of_the_segment (A,B) in L2 holds
L2 = the_perpendicular_bisector (A,B)
let L1, L2 be Element of line_of_REAL 2; :: thesis: ( A <> B & L1 = Line (A,B) & L1 _|_ L2 & the_midpoint_of_the_segment (A,B) in L2 implies L2 = the_perpendicular_bisector (A,B) )
assume that
A1: A <> B and
A2: L1 = Line (A,B) and
A3: L1 _|_ L2 and
A4: the_midpoint_of_the_segment (A,B) in L2 ; :: thesis: L2 = the_perpendicular_bisector (A,B)
set M = the_midpoint_of_the_segment (A,B);
consider L3, L4 being Element of line_of_REAL 2 such that
A5: the_perpendicular_bisector (A,B) = L4 and
A6: L3 = Line (A,B) and
A7: L3 _|_ L4 and
A8: L3 /\ L4 = {(the_midpoint_of_the_segment (A,B))} by A1, Def2;
A9: L2 // L4 by A2, A3, A6, A7, Th13, EUCLIDLP:111;
the_midpoint_of_the_segment (A,B) in L3 /\ L4 by A8, TARSKI:def 1;
then ( the_midpoint_of_the_segment (A,B) in L2 & the_midpoint_of_the_segment (A,B) in L4 ) by A4, XBOOLE_0:def 4;
hence L2 = the_perpendicular_bisector (A,B) by A5, A9, XBOOLE_0:3, EUCLIDLP:71; :: thesis: verum