let A, B be Point of (TOP-REAL 2); ( A <> B implies the_perpendicular_bisector (A,B) = the_perpendicular_bisector (B,A) )
assume A1:
A <> B
; 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; verum