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

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