let L1, L2 be Element of line_of_REAL 2; :: thesis: ( L1 // L2 or ex x being Element of REAL 2 st

( L1 = {x} or L2 = {x} ) or ( L1 is being_line & L2 is being_line & ex x being Element of REAL 2 st L1 /\ L2 = {x} ) )

assume A1: not L1 // L2 ; :: thesis: ( ex x being Element of REAL 2 st

( L1 = {x} or L2 = {x} ) or ( L1 is being_line & L2 is being_line & ex x being Element of REAL 2 st L1 /\ L2 = {x} ) )

set n = 2;

consider x1, x2 being Element of REAL 2 such that

A2: L1 = Line (x1,x2) by EUCLIDLP:51;

consider y1, y2 being Element of REAL 2 such that

A3: L2 = Line (y1,y2) by EUCLIDLP:51;

( x2 - x1 = 0* 2 or y2 - y1 = 0* 2 or for r being Real holds not x2 - x1 = r * (y2 - y1) ) by A1, A2, A3, EUCLIDLP:def 7, EUCLIDLP:def 1;

( L1 = {x} or L2 = {x} ) or ( L1 is being_line & L2 is being_line & ex x being Element of REAL 2 st L1 /\ L2 = {x} ) )

assume A1: not L1 // L2 ; :: thesis: ( ex x being Element of REAL 2 st

( L1 = {x} or L2 = {x} ) or ( L1 is being_line & L2 is being_line & ex x being Element of REAL 2 st L1 /\ L2 = {x} ) )

set n = 2;

consider x1, x2 being Element of REAL 2 such that

A2: L1 = Line (x1,x2) by EUCLIDLP:51;

consider y1, y2 being Element of REAL 2 such that

A3: L2 = Line (y1,y2) by EUCLIDLP:51;

( x2 - x1 = 0* 2 or y2 - y1 = 0* 2 or for r being Real holds not x2 - x1 = r * (y2 - y1) ) by A1, A2, A3, EUCLIDLP:def 7, EUCLIDLP:def 1;

per cases then
( x1 = x2 or y1 = y2 or ( not x1 = x2 & y1 <> y2 & ( for r being Real holds x2 - x1 <> r * (y2 - y1) ) ) )
by EUCLIDLP:9;

end;

suppose
( x1 = x2 or y1 = y2 )
; :: thesis: ( ex x being Element of REAL 2 st

( L1 = {x} or L2 = {x} ) or ( L1 is being_line & L2 is being_line & ex x being Element of REAL 2 st L1 /\ L2 = {x} ) )

( L1 = {x} or L2 = {x} ) or ( L1 is being_line & L2 is being_line & ex x being Element of REAL 2 st L1 /\ L2 = {x} ) )

then
( L1 = {x1} or L2 = {y1} )
by A2, A3, Th3;

hence ( ex x being Element of REAL 2 st

( L1 = {x} or L2 = {x} ) or ( L1 is being_line & L2 is being_line & ex x being Element of REAL 2 st L1 /\ L2 = {x} ) ) ; :: thesis: verum

end;hence ( ex x being Element of REAL 2 st

( L1 = {x} or L2 = {x} ) or ( L1 is being_line & L2 is being_line & ex x being Element of REAL 2 st L1 /\ L2 = {x} ) ) ; :: thesis: verum

suppose A4:
( not x1 = x2 & y1 <> y2 & ( for r being Real holds x2 - x1 <> r * (y2 - y1) ) )
; :: thesis: ( ex x being Element of REAL 2 st

( L1 = {x} or L2 = {x} ) or ( L1 is being_line & L2 is being_line & ex x being Element of REAL 2 st L1 /\ L2 = {x} ) )

( L1 = {x} or L2 = {x} ) or ( L1 is being_line & L2 is being_line & ex x being Element of REAL 2 st L1 /\ L2 = {x} ) )

x2 - x1,y2 - y1 are_lindependent2

A5: Pt in L1 and

A6: Pt in L2 by A2, A3, Th13, EUCLIDLP:114, EUCLIDLP:49;

A7: {Pt} c= L1 /\ L2

hence ( ex x being Element of REAL 2 st

( L1 = {x} or L2 = {x} ) or ( L1 is being_line & L2 is being_line & ex x being Element of REAL 2 st L1 /\ L2 = {x} ) ) by A4, A2, A3; :: thesis: verum

end;proof

then consider Pt being Element of REAL 2 such that
assume
x2 - x1,y2 - y1 are_ldependent2
; :: thesis: contradiction

then ( x2 - x1 = 0* 2 or y2 - y1 = 0* 2 ) by A1, A2, A3, EUCLIDLP:def 7, EUCLIDLP:42;

hence contradiction by A4, EUCLIDLP:9; :: thesis: verum

end;then ( x2 - x1 = 0* 2 or y2 - y1 = 0* 2 ) by A1, A2, A3, EUCLIDLP:def 7, EUCLIDLP:42;

hence contradiction by A4, EUCLIDLP:9; :: thesis: verum

A5: Pt in L1 and

A6: Pt in L2 by A2, A3, Th13, EUCLIDLP:114, EUCLIDLP:49;

A7: {Pt} c= L1 /\ L2

proof

L1 /\ L2 c= {Pt}
let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in {Pt} or t in L1 /\ L2 )

assume t in {Pt} ; :: thesis: t in L1 /\ L2

then t = Pt by TARSKI:def 1;

hence t in L1 /\ L2 by A5, A6, XBOOLE_0:def 4; :: thesis: verum

end;assume t in {Pt} ; :: thesis: t in L1 /\ L2

then t = Pt by TARSKI:def 1;

hence t in L1 /\ L2 by A5, A6, XBOOLE_0:def 4; :: thesis: verum

proof

then
L1 /\ L2 = {Pt}
by A7;
let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in L1 /\ L2 or t in {Pt} )

assume A8: t in L1 /\ L2 ; :: thesis: t in {Pt}

assume not t in {Pt} ; :: thesis: contradiction

then A9: t <> Pt by TARSKI:def 1;

reconsider t1 = t as Element of REAL 2 by A8;

( t1 in L1 & t1 in L2 & Pt in L1 & Pt in L2 ) by A8, A5, A6, XBOOLE_0:def 4;

then ( Line (t1,Pt) = L1 & Line (t1,Pt) = L2 ) by A2, A3, A9, EUCLID_4:10, EUCLID_4:11;

then ( L1 = L2 & L1 is being_line & L2 is being_line ) by A2, A4;

hence contradiction by A1, EUCLIDLP:65; :: thesis: verum

end;assume A8: t in L1 /\ L2 ; :: thesis: t in {Pt}

assume not t in {Pt} ; :: thesis: contradiction

then A9: t <> Pt by TARSKI:def 1;

reconsider t1 = t as Element of REAL 2 by A8;

( t1 in L1 & t1 in L2 & Pt in L1 & Pt in L2 ) by A8, A5, A6, XBOOLE_0:def 4;

then ( Line (t1,Pt) = L1 & Line (t1,Pt) = L2 ) by A2, A3, A9, EUCLID_4:10, EUCLID_4:11;

then ( L1 = L2 & L1 is being_line & L2 is being_line ) by A2, A4;

hence contradiction by A1, EUCLIDLP:65; :: thesis: verum

hence ( ex x being Element of REAL 2 st

( L1 = {x} or L2 = {x} ) or ( L1 is being_line & L2 is being_line & ex x being Element of REAL 2 st L1 /\ L2 = {x} ) ) by A4, A2, A3; :: thesis: verum