let G be _Graph; :: thesis: 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; :: thesis: ( 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 A1:
( not P is closed & not P is chordal )
; :: thesis: 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; :: thesis: ( m < n & n <= len P implies ( not P .cut m,n is chordal & not P .cut m,n is closed ) )
assume A2:
( m < n & n <= len P )
; :: thesis: ( not P .cut m,n is chordal & not P .cut m,n is closed )
set Q = P .cut m,n;
A3:
( m in NAT & n in NAT )
by ORDINAL1:def 13;
now assume
P .cut m,
n is
chordal
;
:: thesis: contradictionthen consider i,
j being
odd Nat such that A4:
(
i + 2
< j &
j <= len (P .cut m,n) &
(P .cut m,n) . i <> (P .cut m,n) . j )
and A5:
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 A6:
e Joins (P .cut m,n) . i,
(P .cut m,n) . j,
G
by A5;
set mi =
(m + i) - 1;
set mj =
(m + j) - 1;
i + 0 < i + 2
by XREAL_1:10;
then
i < j
by A4, XXREAL_0:2;
then
( 1
<= i &
i < len (P .cut m,n) )
by A4, Th2, XXREAL_0:2;
then A7:
i in dom (P .cut m,n)
by FINSEQ_3:27;
then A8:
(
(P .cut m,n) . i = P . ((m + i) - 1) &
(m + i) - 1
in dom P )
by A2, A3, GLIB_001:48;
( 1
<= j &
j <= len (P .cut m,n) )
by A4, Th2;
then
j in dom (P .cut m,n)
by FINSEQ_3:27;
then A9:
(
(P .cut m,n) . j = P . ((m + j) - 1) &
(m + j) - 1
in dom P )
by A2, A3, GLIB_001:48;
reconsider mi =
(m + i) - 1 as
odd Element of
NAT by A8;
reconsider mi =
mi as
odd Nat ;
reconsider mj =
(m + j) - 1 as
odd Element of
NAT by A9;
reconsider mj =
mj as
odd Nat ;
A10:
e Joins P . mi,
P . mj,
G
by A2, A3, A6, A7, A9, GLIB_001:48;
(i + 2) + m < j + m
by A4, XREAL_1:10;
then A11:
((m + i) + 2) - 1
< (m + j) - 1
by XREAL_1:11;
then A12:
mi + 2
< mj
;
mi + 0 < mi + 2
by XREAL_1:10;
then A13:
mi < mj
by A11, XXREAL_0:2;
mj <= len P
by A9, FINSEQ_3:27;
hence
contradiction
by A1, A10, A12, A13, Th92;
:: thesis: verum end;
hence
not P .cut m,n is chordal
; :: thesis: not P .cut m,n is closed
now assume
P .cut m,
n is
closed
;
:: thesis: contradictionthen A14:
(P .cut m,n) .first() = (P .cut m,n) .last()
by GLIB_001:def 24;
(
P . m = (P .cut m,n) .first() &
P . n = (P .cut m,n) .last() )
by A2, A3, GLIB_001:38;
hence
contradiction
by A1, A2, A3, A14, GLIB_001:148;
:: thesis: verum end;
hence
not P .cut m,n is closed
; :: thesis: verum