let L1, L2 be Element of line_of_REAL 2; ( ex L1, L2 being Element of line_of_REAL 2 st
( L1 = L2 & L1 = Line (A,B) & L1 _|_ L2 & L1 /\ L2 = {(the_midpoint_of_the_segment (A,B))} ) & ex L1, L2 being Element of line_of_REAL 2 st
( L2 = L2 & L1 = Line (A,B) & L1 _|_ L2 & L1 /\ L2 = {(the_midpoint_of_the_segment (A,B))} ) implies L1 = L2 )
assume that
A7:
ex D1, D2 being Element of line_of_REAL 2 st
( L1 = D2 & D1 = Line (A,B) & D1 _|_ D2 & D1 /\ D2 = {(the_midpoint_of_the_segment (A,B))} )
and
A8:
ex D3, D4 being Element of line_of_REAL 2 st
( L2 = D4 & D3 = Line (A,B) & D3 _|_ D4 & D3 /\ D4 = {(the_midpoint_of_the_segment (A,B))} )
; L1 = L2
set M = the_midpoint_of_the_segment (A,B);
consider D1, D2 being Element of line_of_REAL 2 such that
A9:
L1 = D2
and
A10:
D1 = Line (A,B)
and
A11:
D1 _|_ D2
and
A12:
D1 /\ D2 = {(the_midpoint_of_the_segment (A,B))}
by A7;
consider D3, D4 being Element of line_of_REAL 2 such that
A13:
L2 = D4
and
A14:
D3 = Line (A,B)
and
A15:
D3 _|_ D4
and
A16:
D3 /\ D4 = {(the_midpoint_of_the_segment (A,B))}
by A8;
A17:
D2 // D4
by A10, A14, A11, A15, Th13, EUCLIDLP:111;
( the_midpoint_of_the_segment (A,B) in D1 /\ D2 & the_midpoint_of_the_segment (A,B) in D1 /\ D4 )
by A10, A14, A12, A16, TARSKI:def 1;
then
( the_midpoint_of_the_segment (A,B) in D2 & the_midpoint_of_the_segment (A,B) in D4 )
by XBOOLE_0:def 4;
hence
L1 = L2
by A9, A13, A17, EUCLIDLP:71, XBOOLE_0:3; verum