let n be Element of NAT ; 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; 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; 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, Th101;
then
L1 meets L2
by A2, Th114;
then consider x0 being Element of REAL n such that
A4:
x0 in L1
and
A5:
x0 in L2
by Th54;
L2 is being_line
by A2, Th72;
then consider x1 being Element of REAL n such that
A6:
x1 <> x0
and
A7:
x1 in L2
by Th58;
A8:
plane (x,x1,x0) c= P
by A1, A3, A4, A7, Th96;
assume that
A9:
L0 // L2
and
A10:
x in L0
; ( L0 c= P & L0 _|_ L1 )
L0 is being_line
by A9, Th71;
then consider x2 being Element of REAL n such that
A11:
( x2 <> x & x2 in L0 )
by Th58;
consider a being Real such that
a <> 0
and
A12:
x2 - x = a * (x1 - x0)
by A9, A10, A5, A6, A7, A11, Th37, Th82;
A13:
(1 + a) + (- a) = 1
;
x2 =
x + (a * (x1 - x0))
by A12, 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:15
;
then A14:
x2 in plane (x,x1,x0)
by A13;
L0 = Line (x2,x)
by A10, A11, Th69;
hence
( L0 c= P & L0 _|_ L1 )
by A2, A3, A9, A14, A8, Th66, Th100; verum