let n be Element of 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, Def12;
consider y2, y3 being Element of REAL n such that
y2 <> y3
and
A5:
L2 = Line y2,y3
by A2, EUCLID_4:def 2;
consider y0, y1 being Element of REAL n such that
A6:
y0 <> y1
and
A7:
L1 = Line y0,y1
by A1, EUCLID_4:def 2;
A8:
y0 - y1 <> 0* n
by A6, Th14;
set P = plane x1,x2,x3;
A9:
y2 in L2
by A5, EUCLID_4:10;
consider y being Element of REAL n such that
A10:
y in Line y0,y1
and
A11:
y0 - y1,y2 - y are_orthogonal
by Th48;
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 Th14;
then A13:
y0 - y1 _|_ y2 - y
by A11, A8, Def3;
consider y9 being Element of REAL n such that
A14:
y <> y9
and
A15:
y9 in L1
by A1, EUCLID_4:15;
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:10;
then A16:
( plane x1,x2,x3 in plane_of_REAL n & y9 - y,y2 - y are_lindependent2 )
by A7, A10, A12, A13, A14, A15, Th45, Th50;
then
plane x1,x2,x3 = plane y,y9,y2
by A4, A7, A9, A10, A15, Th97;
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, Def10; verum