let n be Nat; for L1, L2 being Element of line_of_REAL n st L1,L2 are_coplane & L1 _|_ L2 holds
L1 meets L2
let L1, L2 be Element of line_of_REAL n; ( L1,L2 are_coplane & L1 _|_ L2 implies L1 meets L2 )
assume A1:
L1,L2 are_coplane
; ( not L1 _|_ L2 or L1 meets L2 )
assume A2:
L1 _|_ L2
; L1 meets L2
then A3:
L2 is being_line
by Th67;
L1 is being_line
by A2, Th67;
then consider x0 being Element of REAL n such that
A4:
x0 in L1
and
A5:
not x0 in L2
by A2, A3, Th75, Th79;
consider L being Element of line_of_REAL n such that
A6:
x0 in L
and
A7:
L _|_ L2
and
A8:
L meets L2
by A3, A5, Th62;
consider x being Element of REAL n such that
A9:
x in L
and
A10:
x in L2
by A8, Th49;
x in L1
proof
A11:
L1 meets L
by A4, A6, Th49;
consider P being
Element of
plane_of_REAL n such that
P is
being_plane
and A12:
(
L c= P &
L2 c= P )
by A7, A8, Th107;
consider P0 being
Element of
plane_of_REAL n such that A13:
(
L1 c= P0 &
L2 c= P0 )
by A1, Th96;
A14:
P = P0
by A3, A4, A5, A6, A13, A12, Th102;
consider L0 being
Element of
line_of_REAL n such that A15:
x in L0
and A16:
L0 _|_ L2
and A17:
L0 // L1
by A2, Th80;
assume A18:
not
x in L1
;
contradiction
then consider P1 being
Element of
plane_of_REAL n such that A19:
L0 c= P1
and A20:
L1 c= P1
and
P1 is
being_plane
by A15, A17, Th106;
L1 is
being_line
by A17, Th66;
then
P = P1
by A10, A18, A13, A14, A15, A19, A20, Th102;
then
L = L0
by A7, A9, A10, A12, A15, A16, A19, Th108;
hence
contradiction
by A18, A15, A17, A11, Th71;
verum
end;
hence
L1 meets L2
by A10, Th49; verum