let n be Nat; 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; ( L1,L2 are_coplane & L1 is being_line & L2 is being_line & L1 misses L2 implies L1 // L2 )
assume that
A1:
L1,L2 are_coplane
and
A2:
L1 is being_line
and
A3:
L2 is being_line
; ( not L1 misses L2 or L1 // L2 )
assume A4:
L1 misses L2
; L1 // L2
then consider x being Element of REAL n such that
A5:
x in L1
and
A6:
not x in L2
by Th63;
consider P being Element of plane_of_REAL n such that
A7:
L1 c= P
and
A8:
L2 c= P
by A1, Th96;
consider L9 being Element of line_of_REAL n such that
A9:
x in L9
and
A10:
L9 _|_ L2
and
A11:
L9 meets L2
by A3, A6, Th62;
consider x2 being Element of REAL n such that
A12:
x2 in L9
and
A13:
x2 in L2
by A11, Th49;
consider L0 being Element of line_of_REAL n such that
A14:
x in L0
and
A15:
L0 _|_ L9
and
A16:
L0 // L2
by A10, Th80;
L9 = Line (x2,x)
by A6, A9, A12, A13, Th64;
then A17:
L9 c= P
by A5, A7, A8, A13, Th95;
then A18:
L0 c= P
by A8, A9, A10, A14, A16, Th110;
A19:
L9 is being_line
by A15, Th67;
consider x1 being Element of REAL n such that
A20:
x1 <> x
and
A21:
x1 in L1
by A2, Th53;
A22:
L1 = Line (x,x1)
by A5, A20, A21, Th64;
A23:
L0 meets L1
by A5, A14, Th49;
L1 = L0
proof
A24:
not
x1 in L9
by A4, A9, A11, A20, A22, Th64;
then consider L being
Element of
line_of_REAL n such that A25:
x1 in L
and A26:
L9 _|_ L
and A27:
L9 meets L
by A19, Th62;
A28:
L meets L1
by A21, A25, Th49;
assume
L1 <> L0
;
contradiction
then A29:
L <> L0
by A14, A20, A22, A25, Th64;
consider x9 being
Element of
REAL n such that A30:
x9 in L9
and A31:
x9 in L
by A27, Th49;
L = Line (
x9,
x1)
by A24, A25, A30, A31, Th64;
then A32:
L c= P
by A7, A17, A21, A30, Th95;
then
L // L0
by A17, A15, A18, A26, Th111;
hence
contradiction
by A4, A8, A16, A18, A23, A32, A29, A28, Th112;
verum
end;
hence
L1 // L2
by A16; verum