let A, B be Point of (TOP-REAL 2); 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; ( 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
; 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; verum