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

assume A1: A <> B ; :: thesis: the_perpendicular_bisector (A,B) = the_perpendicular_bisector (B,A)

then consider L1, L2 being Element of line_of_REAL 2 such that

A2: the_perpendicular_bisector (A,B) = L2 and

A3: L1 = Line (A,B) and

A4: L1 _|_ L2 and

A5: L1 /\ L2 = {(the_midpoint_of_the_segment (A,B))} by Def2;

consider L3, L4 being Element of line_of_REAL 2 such that

A6: the_perpendicular_bisector (B,A) = L4 and

A7: L3 = Line (A,B) and

A8: L3 _|_ L4 and

A9: L3 /\ L4 = {(the_midpoint_of_the_segment (B,A))} by A1, Def2;

set M = the_midpoint_of_the_segment (A,B);

consider x being Element of REAL 2 such that

A10: L1 /\ L2 = {x} by A4, Th33;

consider y being Element of REAL 2 such that

A11: L3 /\ L4 = {y} by A8, Th33;

A12: L2 // L4 by A3, A4, A7, A8, Th13, EUCLIDLP:111;

( {x} = {(the_midpoint_of_the_segment (A,B))} & {y} = {(the_midpoint_of_the_segment (A,B))} ) by A5, A9, A10, A11, Th23;

then ( the_midpoint_of_the_segment (A,B) in L1 /\ L2 & the_midpoint_of_the_segment (A,B) in L3 /\ L4 ) by A10, A11, TARSKI:def 1;

then ( the_midpoint_of_the_segment (A,B) in L1 & the_midpoint_of_the_segment (A,B) in L2 & the_midpoint_of_the_segment (A,B) in L3 & the_midpoint_of_the_segment (A,B) in L4 ) by XBOOLE_0:def 4;

hence the_perpendicular_bisector (A,B) = the_perpendicular_bisector (B,A) by A2, A6, A12, XBOOLE_0:3, EUCLIDLP:71; :: thesis: verum

assume A1: A <> B ; :: thesis: the_perpendicular_bisector (A,B) = the_perpendicular_bisector (B,A)

then consider L1, L2 being Element of line_of_REAL 2 such that

A2: the_perpendicular_bisector (A,B) = L2 and

A3: L1 = Line (A,B) and

A4: L1 _|_ L2 and

A5: L1 /\ L2 = {(the_midpoint_of_the_segment (A,B))} by Def2;

consider L3, L4 being Element of line_of_REAL 2 such that

A6: the_perpendicular_bisector (B,A) = L4 and

A7: L3 = Line (A,B) and

A8: L3 _|_ L4 and

A9: L3 /\ L4 = {(the_midpoint_of_the_segment (B,A))} by A1, Def2;

set M = the_midpoint_of_the_segment (A,B);

consider x being Element of REAL 2 such that

A10: L1 /\ L2 = {x} by A4, Th33;

consider y being Element of REAL 2 such that

A11: L3 /\ L4 = {y} by A8, Th33;

A12: L2 // L4 by A3, A4, A7, A8, Th13, EUCLIDLP:111;

( {x} = {(the_midpoint_of_the_segment (A,B))} & {y} = {(the_midpoint_of_the_segment (A,B))} ) by A5, A9, A10, A11, Th23;

then ( the_midpoint_of_the_segment (A,B) in L1 /\ L2 & the_midpoint_of_the_segment (A,B) in L3 /\ L4 ) by A10, A11, TARSKI:def 1;

then ( the_midpoint_of_the_segment (A,B) in L1 & the_midpoint_of_the_segment (A,B) in L2 & the_midpoint_of_the_segment (A,B) in L3 & the_midpoint_of_the_segment (A,B) in L4 ) by XBOOLE_0:def 4;

hence the_perpendicular_bisector (A,B) = the_perpendicular_bisector (B,A) by A2, A6, A12, XBOOLE_0:3, EUCLIDLP:71; :: thesis: verum