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;
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;
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} ) )
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;
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} ) )
x2 - x1,y2 - y1 are_lindependent2
proof
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 consider Pt being Element of REAL 2 such that
A5: Pt in L1 and
A6: Pt in L2 by A2, A3, Th13, EUCLIDLP:114, EUCLIDLP:49;
A7: {Pt} c= L1 /\ L2
proof
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;
L1 /\ L2 c= {Pt}
proof
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;
then L1 /\ L2 = {Pt} by A7;
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;
end;