let n be Element of 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 Th72;
L1 is being_line
by A2, Th72;
then consider x0 being Element of REAL n such that
A4:
x0 in L1
and
A5:
not x0 in L2
by A2, A3, Th80, Th84;
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, Th67;
consider x being Element of REAL n such that
A9:
x in L
and
A10:
x in L2
by A8, Th54;
x in L1
proof
A11:
L1 meets L
by A4, A6, Th54;
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, Th112;
consider P0 being
Element of
plane_of_REAL n such that A13:
(
L1 c= P0 &
L2 c= P0 )
by A1, Th101;
A14:
P = P0
by A3, A4, A5, A6, A13, A12, Th107;
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, Th85;
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, Th111;
L1 is
being_line
by A17, Th71;
then
P = P1
by A10, A18, A13, A14, A15, A19, A20, Th107;
then
L = L0
by A7, A9, A10, A12, A15, A16, A19, Th113;
hence
contradiction
by A18, A15, A17, A11, Th76;
verum
end;
hence
L1 meets L2
by A10, Th54; verum