let n be Nat; for L1, L2 being Element of line_of_REAL n st L1 is being_line & L2 is being_line & L1,L2 are_coplane & L1 misses L2 holds
ex P being Element of plane_of_REAL n st
( L1 c= P & L2 c= P & P is being_plane )
let L1, L2 be Element of line_of_REAL n; ( L1 is being_line & L2 is being_line & L1,L2 are_coplane & L1 misses L2 implies ex P being Element of plane_of_REAL n st
( L1 c= P & L2 c= P & P is being_plane ) )
assume that
A1:
L1 is being_line
and
A2:
L2 is being_line
and
A3:
L1,L2 are_coplane
; ( not L1 misses L2 or ex P being Element of plane_of_REAL n st
( L1 c= P & L2 c= P & P is being_plane ) )
consider x1, x2, x3 being Element of REAL n such that
A4:
( L1 c= plane (x1,x2,x3) & L2 c= plane (x1,x2,x3) )
by A3;
consider y2, y3 being Element of REAL n such that
y2 <> y3
and
A5:
L2 = Line (y2,y3)
by A2;
consider y0, y1 being Element of REAL n such that
A6:
y0 <> y1
and
A7:
L1 = Line (y0,y1)
by A1;
A8:
y0 - y1 <> 0* n
by A6, Th9;
set P = plane (x1,x2,x3);
A9:
y2 in L2
by A5, EUCLID_4:9;
consider y being Element of REAL n such that
A10:
y in Line (y0,y1)
and
A11:
y0 - y1,y2 - y are_orthogonal
by Th43;
assume
L1 misses L2
; ex P being Element of plane_of_REAL n st
( L1 c= P & L2 c= P & P is being_plane )
then A12:
y <> y2
by A7, A9, A10, XBOOLE_0:3;
then
y2 - y <> 0* n
by Th9;
then A13:
y0 - y1 _|_ y2 - y
by A11, A8;
consider y9 being Element of REAL n such that
A14:
y <> y9
and
A15:
y9 in L1
by A1, EUCLID_4:14;
take
plane (x1,x2,x3)
; ( plane (x1,x2,x3) is Element of plane_of_REAL n & L1 c= plane (x1,x2,x3) & L2 c= plane (x1,x2,x3) & plane (x1,x2,x3) is being_plane )
( y in Line (y,y2) & y2 in Line (y,y2) )
by EUCLID_4:9;
then A16:
( plane (x1,x2,x3) in plane_of_REAL n & y9 - y,y2 - y are_lindependent2 )
by A7, A10, A12, A13, A14, A15, Th40, Th45;
then
plane (x1,x2,x3) = plane (y,y9,y2)
by A4, A7, A9, A10, A15, Th92;
hence
( plane (x1,x2,x3) is Element of plane_of_REAL n & L1 c= plane (x1,x2,x3) & L2 c= plane (x1,x2,x3) & plane (x1,x2,x3) is being_plane )
by A4, A16; verum