let G be _Graph; for P being Path of G st not P is closed & not P is chordal holds
for m, n being natural odd number st m < n & n <= len P holds
( not P .cut (m,n) is chordal & not P .cut (m,n) is closed )
let P be Path of G; ( not P is closed & not P is chordal implies for m, n being natural odd number st m < n & n <= len P holds
( not P .cut (m,n) is chordal & not P .cut (m,n) is closed ) )
assume that
A1:
not P is closed
and
A2:
not P is chordal
; for m, n being natural odd number st m < n & n <= len P holds
( not P .cut (m,n) is chordal & not P .cut (m,n) is closed )
let m, n be odd Nat; ( m < n & n <= len P implies ( not P .cut (m,n) is chordal & not P .cut (m,n) is closed ) )
assume that
A3:
m < n
and
A4:
n <= len P
; ( not P .cut (m,n) is chordal & not P .cut (m,n) is closed )
set Q = P .cut (m,n);
A5:
n in NAT
by ORDINAL1:def 13;
A6:
m in NAT
by ORDINAL1:def 13;
now assume
P .cut (
m,
n) is
chordal
;
contradictionthen consider i,
j being
odd Nat such that A7:
i + 2
< j
and A8:
j <= len (P .cut (m,n))
and
(P .cut (m,n)) . i <> (P .cut (m,n)) . j
and A9:
ex
e being
set st
e Joins (P .cut (m,n)) . i,
(P .cut (m,n)) . j,
G
and
for
f being
set st
f in (P .cut (m,n)) .edges() holds
not
f Joins (P .cut (m,n)) . i,
(P .cut (m,n)) . j,
G
by Def10;
consider e being
set such that A10:
e Joins (P .cut (m,n)) . i,
(P .cut (m,n)) . j,
G
by A9;
set mi =
(m + i) - 1;
set mj =
(m + j) - 1;
1
<= j
by Th2;
then A11:
j in dom (P .cut (m,n))
by A8, FINSEQ_3:27;
then A12:
(P .cut (m,n)) . j = P . ((m + j) - 1)
by A3, A4, A6, A5, GLIB_001:48;
A13:
(m + j) - 1
in dom P
by A3, A4, A6, A5, A11, GLIB_001:48;
i + 0 < i + 2
by XREAL_1:10;
then
i < j
by A7, XXREAL_0:2;
then A14:
i < len (P .cut (m,n))
by A8, XXREAL_0:2;
1
<= i
by Th2;
then A15:
i in dom (P .cut (m,n))
by A14, FINSEQ_3:27;
then A16:
(m + i) - 1
in dom P
by A3, A4, A6, A5, GLIB_001:48;
reconsider mj =
(m + j) - 1 as
odd Element of
NAT by A13;
reconsider mj =
mj as
odd Nat ;
A17:
mj <= len P
by A13, FINSEQ_3:27;
reconsider mi =
(m + i) - 1 as
odd Element of
NAT by A16;
reconsider mi =
mi as
odd Nat ;
(i + 2) + m < j + m
by A7, XREAL_1:10;
then A18:
((m + i) + 2) - 1
< (m + j) - 1
by XREAL_1:11;
then A19:
mi + 2
< mj
;
mi + 0 < mi + 2
by XREAL_1:10;
then A20:
mi < mj
by A18, XXREAL_0:2;
e Joins P . mi,
P . mj,
G
by A3, A4, A6, A5, A10, A15, A12, GLIB_001:48;
hence
contradiction
by A1, A2, A19, A20, A17, Th92;
verum end;
hence
not P .cut (m,n) is chordal
; not P .cut (m,n) is closed
now assume
P .cut (
m,
n) is
closed
;
contradictionthen A21:
(P .cut (m,n)) .first() = (P .cut (m,n)) .last()
by GLIB_001:def 24;
A22:
P . n = (P .cut (m,n)) .last()
by A3, A4, A6, A5, GLIB_001:38;
P . m = (P .cut (m,n)) .first()
by A3, A4, A6, A5, GLIB_001:38;
hence
contradiction
by A1, A3, A4, A6, A5, A21, A22, GLIB_001:148;
verum end;
hence
not P .cut (m,n) is closed
; verum