let n be Element of NAT ; :: thesis: for L0, L1, L2, L being Element of line_of_REAL n
for P being Element of plane_of_REAL n st L0 c= P & L1 c= P & L2 c= P & L0 // L1 & L1 // L2 & L0 <> L1 & L1 <> L2 & L2 <> L0 & L meets L0 & L meets L1 holds
L meets L2
let L0, L1, L2, L be Element of line_of_REAL n; :: thesis: for P being Element of plane_of_REAL n st L0 c= P & L1 c= P & L2 c= P & L0 // L1 & L1 // L2 & L0 <> L1 & L1 <> L2 & L2 <> L0 & L meets L0 & L meets L1 holds
L meets L2
let P be Element of plane_of_REAL n; :: thesis: ( L0 c= P & L1 c= P & L2 c= P & L0 // L1 & L1 // L2 & L0 <> L1 & L1 <> L2 & L2 <> L0 & L meets L0 & L meets L1 implies L meets L2 )
assume A1: ( L0 c= P & L1 c= P & L2 c= P & L0 // L1 & L1 // L2 & L0 <> L1 & L1 <> L2 & L2 <> L0 ) ; :: thesis: ( not L meets L0 or not L meets L1 or L meets L2 )
then A2: ( L0 is being_line & L1 is being_line & L2 is being_line ) by Th71;
assume A3: ( L meets L0 & L meets L1 ) ; :: thesis: L meets L2
then consider x0 being Element of REAL n such that
A4: ( x0 in L & x0 in L0 ) by Th54;
consider x1 being Element of REAL n such that
A5: ( x1 in L & x1 in L1 ) by A3, Th54;
A6: ( L0 misses L1 & L1 misses L2 & L0 misses L2 ) by A1, Th65, Th76;
then ( not x0 in L1 & not x0 in L2 & not x1 in L0 & not x1 in L2 ) by A4, A5, Th54;
then consider L' being Element of line_of_REAL n such that
A7: ( x0 in L' & L' _|_ L1 & L' meets L1 ) by A2, Th67;
consider y1 being Element of REAL n such that
A8: ( y1 in L' & y1 in L1 ) by A7, Th54;
A9: x0 <> y1 by A4, A6, A8, Th54;
then A10: ( L' = Line x0,y1 & L' is being_line ) by A7, A8, Th69;
then L' c= P by A1, A4, A8, Th100;
then L',L2 are_coplane by A1, Th101;
then A11: L' meets L2 by A1, A7, Th66, Th114;
then consider y2 being Element of REAL n such that
A12: ( y2 in L' & y2 in L2 ) by Th54;
consider x2 being Element of REAL n such that
A13: ( x2 <> y2 & x2 in L2 ) by A2, A12, Th58;
A14: L2 = Line y2,x2 by A12, A13, Th69;
consider a being Real such that
A15: y2 - x0 = a * (y1 - x0) by A7, A8, A9, A12, Th75;
x0 <> x1 by A4, A5, A6, Th54;
then A16: L = Line x0,x1 by A4, A5, Th69;

now

per cases ( x1 = y1 or x1 <> y1 ) ;

case x1 = y1 ; :: thesis: L meets L2

hence L meets L2 by A4, A5, A9, A10, A11, Th69; :: thesis: verum

end;

case x1 <> y1 ; :: thesis: L meets L2

then x2 - y2 // x1 - y1 by A1, A5, A8, A12, A13, Th82;
then consider b being Real such that
A17: ( b <> 0 & x2 - y2 = b * (x1 - y1) ) by Th37;
A18: x1 - y1 = 1 * (x1 - y1) by EUCLID_4:3
.= ((1 / b) * b) * (x1 - y1) by A17, XCMPLX_1:88
.= (1 / b) * (x2 - y2) by A17, EUCLID_4:4 ;
set x = ((1 - a) * x0) + (a * x1);
A19: ((1 - a) * x0) + (a * x1) in L by A16;
((1 - a) * x0) + (a * x1) = ((1 * x0) + (- (a * x0))) + (a * x1) by Th16
.= (x0 + (- (a * x0))) + (a * x1) by EUCLID_4:3
.= ((a * x1) + (- (a * x0))) + x0 by RVSUM_1:32
.= (a * (x1 - x0)) + x0 by Th17
.= (a * ((x1 + (0* n)) + (- x0))) + x0 by EUCLID_4:1
.= (a * ((x1 + ((- y1) + y1)) + (- x0))) + x0 by Th7
.= (a * (((x1 + (- y1)) + y1) + (- x0))) + x0 by RVSUM_1:32
.= (a * ((x1 - y1) + (y1 + (- x0)))) + x0 by RVSUM_1:32
.= ((a * ((1 / b) * (x2 - y2))) + (a * (y1 - x0))) + x0 by A18, EUCLID_4:6
.= (((a * (1 / b)) * (x2 - y2)) + (a * (y1 - x0))) + x0 by EUCLID_4:4
.= (((a / b) * (x2 - y2)) + (a * (y1 - x0))) + x0 by XCMPLX_1:100
.= ((a / b) * (x2 - y2)) + ((y2 + (- x0)) + x0) by A15, RVSUM_1:32
.= ((a / b) * (x2 - y2)) + (y2 + ((- x0) + x0)) by RVSUM_1:32
.= ((a / b) * (x2 - y2)) + (y2 + (0* n)) by Th7
.= ((a / b) * (x2 - y2)) + y2 by EUCLID_4:1
.= (((a / b) * x2) + (- ((a / b) * y2))) + y2 by Th17
.= (y2 + (- ((a / b) * y2))) + ((a / b) * x2) by RVSUM_1:32
.= ((1 * y2) + (- ((a / b) * y2))) + ((a / b) * x2) by EUCLID_4:3
.= ((1 - (a / b)) * y2) + ((a / b) * x2) by Th16 ;
then ((1 - a) * x0) + (a * x1) in L2 by A14;
hence L meets L2 by A19, Th54; :: thesis: verum

end;

end;

end;

hence L meets L2 ; :: thesis: verum