let n be Element of NAT ; :: thesis: for x being Element of REAL n
for L1, L2, L0 being Element of line_of_REAL n
for P being Element of plane_of_REAL n st L1 c= P & L2 c= P & L1 _|_ L2 & x in P & L0 // L2 & x in L0 holds
( L0 c= P & L0 _|_ L1 )
let x be Element of REAL n; :: thesis: for L1, L2, L0 being Element of line_of_REAL n
for P being Element of plane_of_REAL n st L1 c= P & L2 c= P & L1 _|_ L2 & x in P & L0 // L2 & x in L0 holds
( L0 c= P & L0 _|_ L1 )
let L1, L2, L0 be Element of line_of_REAL n; :: thesis: for P being Element of plane_of_REAL n st L1 c= P & L2 c= P & L1 _|_ L2 & x in P & L0 // L2 & x in L0 holds
( L0 c= P & L0 _|_ L1 )
let P be Element of plane_of_REAL n; :: thesis: ( L1 c= P & L2 c= P & L1 _|_ L2 & x in P & L0 // L2 & x in L0 implies ( L0 c= P & L0 _|_ L1 ) )
assume A1: ( L1 c= P & L2 c= P & L1 _|_ L2 & x in P ) ; :: thesis: ( not L0 // L2 or not x in L0 or ( L0 c= P & L0 _|_ L1 ) )
assume A2: ( L0 // L2 & x in L0 ) ; :: thesis: ( L0 c= P & L0 _|_ L1 )
L1,L2 are_coplane by A1, Th101;
then L1 meets L2 by A1, Th114;
then consider x0 being Element of REAL n such that
A3: ( x0 in L1 & x0 in L2 ) by Th54;
( L1 is being_line & L2 is being_line ) by A1, Th72;
then consider x1 being Element of REAL n such that
A4: ( x1 <> x0 & x1 in L2 ) by A3, Th58;
L0 is being_line by A2, Th71;
then consider x2 being Element of REAL n such that
A5: ( x2 <> x & x2 in L0 ) by A2, Th58;
A6: L0 = Line x2,x by A2, A5, Th69;
x2 - x // x1 - x0 by A2, A3, A4, A5, Th82;
then consider a being Real such that
A7: ( a <> 0 & x2 - x = a * (x1 - x0) ) by Th37;
A8: x2 = x + (a * (x1 - x0)) by A7, Th11
.= (1 * x) + (a * (x1 - x0)) by EUCLID_4:3
.= (1 * x) + ((a * x1) + ((- a) * x0)) by Th17
.= ((1 * x) + (a * x1)) + ((- a) * x0) by RVSUM_1:32 ;
(1 + a) + (- a) = 1 ;
then A9: x2 in plane x,x1,x0 by A8;
plane x,x1,x0 c= P by A1, A3, A4, Th96;
hence ( L0 c= P & L0 _|_ L1 ) by A1, A2, A6, A9, Th66, Th100; :: thesis: verum