let G be _Graph; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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; :: thesis: ( 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 ; :: thesis: ( 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 :: thesis: not P .cut (m,n) is chordal
assume P .cut (m,n) is chordal ; :: thesis: contradiction
then 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 ;
then A12: (P .cut (m,n)) . j = P . ((m + j) - 1) by ;
A13: (m + j) - 1 in dom P by ;
i + 0 < i + 2 by XREAL_1:8;
then i < j by ;
then A14: i < len (P .cut (m,n)) by ;
1 <= i by Th2;
then A15: i in dom (P .cut (m,n)) by ;
then A16: (m + i) - 1 in dom P by ;
reconsider mj = (m + j) - 1 as odd Element of NAT by A13;
reconsider mj = mj as odd Nat ;
A17: mj <= len P by ;
reconsider mi = (m + i) - 1 as odd Element of NAT by A16;
reconsider mi = mi as odd Nat ;
(i + 2) + m < j + m by ;
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 ;
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; :: thesis: verum
end;
hence P .cut (m,n) is chordless ; :: thesis: P .cut (m,n) is open
now :: thesis: not P .cut (m,n) is closed
assume P .cut (m,n) is closed ; :: thesis: contradiction
then A21: (P .cut (m,n)) .first() = (P .cut (m,n)) .last() ;
A22: P . n = (P .cut (m,n)) .last() by ;
P . m = (P .cut (m,n)) .first() by ;
hence contradiction by A1, A3, A4, A6, A5, A21, A22, GLIB_001:147; :: thesis: verum
end;
hence P .cut (m,n) is open ; :: thesis: verum