let G be _Graph; for P being Path of G st P is open & P is chordless holds
for m, n being odd Nat st m < n & n <= len P holds
( P .cut (m,n) is chordless & P .cut (m,n) is open )
let P be Path of G; ( P is open & P is chordless implies for m, n being odd Nat st m < n & n <= len P holds
( P .cut (m,n) is chordless & P .cut (m,n) is open ) )
assume that
A1:
P is open
and
A2:
P is chordless
; for m, n being odd Nat st m < n & n <= len P holds
( P .cut (m,n) is chordless & P .cut (m,n) is open )
let m, n be odd Nat; ( m < n & n <= len P implies ( P .cut (m,n) is chordless & P .cut (m,n) is open ) )
assume that
A3:
m < n
and
A4:
n <= len P
; ( P .cut (m,n) is chordless & P .cut (m,n) is open )
set Q = P .cut (m,n);
A5:
n in NAT
by ORDINAL1:def 12;
A6:
m in NAT
by ORDINAL1:def 12;
now not P .cut (m,n) is chordal 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
object st
e Joins (P .cut (m,n)) . i,
(P .cut (m,n)) . j,
G
and
for
f being
object st
f in (P .cut (m,n)) .edges() holds
not
f Joins (P .cut (m,n)) . i,
(P .cut (m,n)) . j,
G
;
consider e being
object 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:25;
then A12:
(P .cut (m,n)) . j = P . ((m + j) - 1)
by A3, A4, A6, A5, GLIB_001:47;
A13:
(m + j) - 1
in dom P
by A3, A4, A6, A5, A11, GLIB_001:47;
i + 0 < i + 2
by XREAL_1:8;
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:25;
then A16:
(m + i) - 1
in dom P
by A3, A4, A6, A5, GLIB_001:47;
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:25;
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:8;
then A18:
((m + i) + 2) - 1
< (m + j) - 1
by XREAL_1:9;
then A19:
mi + 2
< mj
;
mi + 0 < mi + 2
by XREAL_1:8;
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:47;
hence
contradiction
by A1, A2, A19, A20, A17, Th91;
verum end;
hence
P .cut (m,n) is chordless
; P .cut (m,n) is open
now not P .cut (m,n) is closed assume
P .cut (
m,
n) is
closed
;
contradictionthen A21:
(P .cut (m,n)) .first() = (P .cut (m,n)) .last()
;
A22:
P . n = (P .cut (m,n)) .last()
by A3, A4, A6, A5, GLIB_001:37;
P . m = (P .cut (m,n)) .first()
by A3, A4, A6, A5, GLIB_001:37;
hence
contradiction
by A1, A3, A4, A6, A5, A21, A22, GLIB_001:147;
verum end;
hence
P .cut (m,n) is open
; verum