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;

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

hence
P .cut (m,n) is chordless
; :: thesis: P .cut (m,n) is open 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 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; :: thesis: verum

end;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 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; :: thesis: verum

now :: thesis: not P .cut (m,n) is closed

hence
P .cut (m,n) is open
; :: thesis: verumassume
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 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; :: thesis: verum

end;then 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; :: thesis: verum