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

( 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