let L1, L2 be Element of line_of_REAL 2; :: thesis: ( ex L1, L2 being Element of line_of_REAL 2 st
( L1 = L1 & L2 = Line (B,C) & A in L1 & L1 _|_ L2 ) & ex L1, L2 being Element of line_of_REAL 2 st
( L2 = L1 & L2 = Line (B,C) & A in L1 & L1 _|_ L2 ) implies L1 = L2 )
assume that
A4: ex L11, L12 being Element of line_of_REAL 2 st
( L1 = L11 & L12 = Line (B,C) & A in L11 & L11 _|_ L12 ) and
A5: ex L21, L22 being Element of line_of_REAL 2 st
( L2 = L21 & L22 = Line (B,C) & A in L21 & L21 _|_ L22 ) ; :: thesis: L1 = L2
consider L11, L12 being Element of line_of_REAL 2 such that
A6: L1 = L11 and
A7: L12 = Line (B,C) and
A8: A in L11 and
A9: L11 _|_ L12 by A4;
consider L21, L22 being Element of line_of_REAL 2 such that
A10: L2 = L21 and
A11: L22 = Line (B,C) and
A12: A in L21 and
A13: L21 _|_ L22 by A5;
not L11 misses L21 by A8, A12, XBOOLE_0:def 4;
hence L1 = L2 by A6, A10, EUCLIDLP:71, A7, A11, EUCLID12:16, A9, A13, EUCLIDLP:111; :: thesis: verum