let n be Nat; for x being Element of REAL n
for L0, L1, L2 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; for L0, L1, L2 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 L0, L1, L2 be 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 P be Element of plane_of_REAL n; ( L1 c= P & L2 c= P & L1 _|_ L2 & x in P & L0 // L2 & x in L0 implies ( L0 c= P & L0 _|_ L1 ) )
assume that
A1:
( L1 c= P & L2 c= P )
and
A2:
L1 _|_ L2
and
A3:
x in P
; ( not L0 // L2 or not x in L0 or ( L0 c= P & L0 _|_ L1 ) )
L1,L2 are_coplane
by A1, Th96;
then
L1 meets L2
by A2, Th109;
then consider x0 being Element of REAL n such that
A4:
x0 in L1
and
A5:
x0 in L2
by Th49;
L2 is being_line
by A2, Th67;
then consider x1 being Element of REAL n such that
A6:
x1 <> x0
and
A7:
x1 in L2
by Th53;
A8:
plane (x,x1,x0) c= P
by A1, A3, A4, A7, Th91;
assume that
A9:
L0 // L2
and
A10:
x in L0
; ( L0 c= P & L0 _|_ L1 )
L0 is being_line
by A9, Th66;
then consider x2 being Element of REAL n such that
A11:
( x2 <> x & x2 in L0 )
by Th53;
consider a being Real such that
a <> 0
and
A12:
x2 - x = a * (x1 - x0)
by A9, A10, A5, A6, A7, A11, Th32, Th77;
A13:
(1 + a) + (- a) = 1
;
x2 =
x + (a * (x1 - x0))
by A12, Th6
.=
(1 * x) + (a * (x1 - x0))
by EUCLID_4:3
.=
(1 * x) + ((a * x1) + ((- a) * x0))
by Th12
.=
((1 * x) + (a * x1)) + ((- a) * x0)
by RVSUM_1:15
;
then A14:
x2 in plane (x,x1,x0)
by A13;
L0 = Line (x2,x)
by A10, A11, Th64;
hence
( L0 c= P & L0 _|_ L1 )
by A2, A3, A9, A14, A8, Th61, Th95; verum