let L1, L2 be Element of line_of_REAL 2; :: thesis: ( 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))} ) ; :: thesis: 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; :: thesis: verum