let n be Element of NAT ; :: thesis: for L1, L2 being Element of line_of_REAL n st L1,L2 are_coplane & L1 is being_line & L2 is being_line & L1 misses L2 holds
L1 // L2
let L1, L2 be Element of line_of_REAL n; :: thesis: ( L1,L2 are_coplane & L1 is being_line & L2 is being_line & L1 misses L2 implies L1 // L2 )
assume A1:
( L1,L2 are_coplane & L1 is being_line & L2 is being_line )
; :: thesis: ( not L1 misses L2 or L1 // L2 )
assume A2:
L1 misses L2
; :: thesis: L1 // L2
then consider x being Element of REAL n such that
A3:
( x in L1 & not x in L2 )
by Th68;
consider P being Element of plane_of_REAL n such that
A4:
( L1 c= P & L2 c= P )
by A1, Th101;
consider L' being Element of line_of_REAL n such that
A5:
( x in L' & L' _|_ L2 & L' meets L2 )
by A1, A3, Th67;
consider x2 being Element of REAL n such that
A6:
( x2 in L' & x2 in L2 )
by A5, Th54;
( L' = Line x2,x & L' is being_line )
by A3, A5, A6, Th69;
then A7:
L' c= P
by A3, A4, A6, Th100;
consider L0 being Element of line_of_REAL n such that
A8:
( x in L0 & L0 _|_ L' & L0 // L2 )
by A5, Th85;
A9:
L0 c= P
by A4, A5, A7, A8, Th115;
A10:
L0 meets L1
by A3, A8, Th54;
A11:
( L0 is being_line & L' is being_line )
by A8, Th72;
consider x1 being Element of REAL n such that
A12:
( x1 <> x & x1 in L1 )
by A1, A3, Th58;
A13:
L1 = Line x,x1
by A3, A12, Th69;
L1 = L0
proof
assume A14:
L1 <> L0
;
:: thesis: contradiction
A15:
not
x1 in L'
by A2, A5, A12, A13, Th69;
then consider L being
Element of
line_of_REAL n such that A16:
(
x1 in L &
L' _|_ L &
L' meets L )
by A11, Th67;
consider x' being
Element of
REAL n such that A17:
(
x' in L' &
x' in L )
by A16, Th54;
L = Line x',
x1
by A15, A16, A17, Th69;
then A18:
L c= P
by A4, A7, A12, A17, Th100;
A19:
L <> L0
by A8, A12, A13, A14, A16, Th69;
A20:
L // L0
by A7, A8, A9, A16, A18, Th116;
A21:
L <> L2
by A2, A12, A16, Th54;
L meets L1
by A12, A16, Th54;
hence
contradiction
by A2, A3, A4, A8, A9, A10, A18, A19, A20, A21, Th117;
:: thesis: verum
end;
hence
L1 // L2
by A8; :: thesis: verum