let G be _Graph; :: thesis: for W being Walk of G st W is chordal holds

ex m, n being odd Nat st

( m + 2 < n & n <= len W & W . m <> W . n & ex e being object st e Joins W . m,W . n,G & ( W is Cycle-like implies ( ( not m = 1 or not n = len W ) & ( not m = 1 or not n = (len W) - 2 ) & ( not m = 3 or not n = len W ) ) ) )

let W be Walk of G; :: thesis: ( W is chordal implies ex m, n being odd Nat st

( m + 2 < n & n <= len W & W . m <> W . n & ex e being object st e Joins W . m,W . n,G & ( W is Cycle-like implies ( ( not m = 1 or not n = len W ) & ( not m = 1 or not n = (len W) - 2 ) & ( not m = 3 or not n = len W ) ) ) ) )

given m, n being odd Nat such that A1: m + 2 < n and

A2: n <= len W and

A3: W . m <> W . n and

A4: ex e being object st e Joins W . m,W . n,G and

A5: for f being object st f in W .edges() holds

not f Joins W . m,W . n,G ; :: according to CHORD:def 10 :: thesis: ex m, n being odd Nat st

( m + 2 < n & n <= len W & W . m <> W . n & ex e being object st e Joins W . m,W . n,G & ( W is Cycle-like implies ( ( not m = 1 or not n = len W ) & ( not m = 1 or not n = (len W) - 2 ) & ( not m = 3 or not n = len W ) ) ) )

take m ; :: thesis: ex n being odd Nat st

( m + 2 < n & n <= len W & W . m <> W . n & ex e being object st e Joins W . m,W . n,G & ( W is Cycle-like implies ( ( not m = 1 or not n = len W ) & ( not m = 1 or not n = (len W) - 2 ) & ( not m = 3 or not n = len W ) ) ) )

take n ; :: thesis: ( m + 2 < n & n <= len W & W . m <> W . n & ex e being object st e Joins W . m,W . n,G & ( W is Cycle-like implies ( ( not m = 1 or not n = len W ) & ( not m = 1 or not n = (len W) - 2 ) & ( not m = 3 or not n = len W ) ) ) )

thus m + 2 < n by A1; :: thesis: ( n <= len W & W . m <> W . n & ex e being object st e Joins W . m,W . n,G & ( W is Cycle-like implies ( ( not m = 1 or not n = len W ) & ( not m = 1 or not n = (len W) - 2 ) & ( not m = 3 or not n = len W ) ) ) )

thus n <= len W by A2; :: thesis: ( W . m <> W . n & ex e being object st e Joins W . m,W . n,G & ( W is Cycle-like implies ( ( not m = 1 or not n = len W ) & ( not m = 1 or not n = (len W) - 2 ) & ( not m = 3 or not n = len W ) ) ) )

thus W . m <> W . n by A3; :: thesis: ( ex e being object st e Joins W . m,W . n,G & ( W is Cycle-like implies ( ( not m = 1 or not n = len W ) & ( not m = 1 or not n = (len W) - 2 ) & ( not m = 3 or not n = len W ) ) ) )

thus ex e being object st e Joins W . m,W . n,G by A4; :: thesis: ( W is Cycle-like implies ( ( not m = 1 or not n = len W ) & ( not m = 1 or not n = (len W) - 2 ) & ( not m = 3 or not n = len W ) ) )

A6: W .last() = W . (len W) ;

assume A7: W is Cycle-like ; :: thesis: ( ( not m = 1 or not n = len W ) & ( not m = 1 or not n = (len W) - 2 ) & ( not m = 3 or not n = len W ) )

then A8: 3 <= len W by GLIB_001:125;

then reconsider lW2 = (len W) - (2 * 1) as odd Element of NAT by INT_1:5, XXREAL_0:2;

A9: W .first() = W . 1 ;

then A10: W . 1 = W . (len W) by A7, A6, GLIB_001:def 24;

reconsider lW2 = lW2 as odd Nat ;

reconsider le = lW2 + 1 as even Nat ;

A11: 1 <= le by NAT_1:12;

A12: lW2 < len W by XREAL_1:44;

then A13: le <= len W by NAT_1:13;

then le div 2 in dom (W .edgeSeq()) by A11, GLIB_001:77;

then (W .edgeSeq()) . (le div 2) in rng (W .edgeSeq()) by FUNCT_1:3;

then A14: W . (((len W) - 2) + 1) in W .edges() by A11, A13, GLIB_001:77;

thus ( not m = 1 or not n = len W ) by A3, A7, A9, A6, GLIB_001:def 24; :: thesis: ( ( not m = 1 or not n = (len W) - 2 ) & ( not m = 3 or not n = len W ) )

W . (lW2 + 1) Joins W . lW2,W . (lW2 + 2),G by A12, GLIB_001:def 3;

hence ( not m = 1 or not n = (len W) - 2 ) by A5, A10, A14, GLIB_000:14; :: thesis: ( not m = 3 or not n = len W )

A15: (2 * 0) + 1 is odd Nat ;

A16: (2 * 1) div 2 = 1 by NAT_D:18;

A17: 1 + 1 <= len W by A8, XXREAL_0:2;

then 1 in dom (W .edgeSeq()) by A16, GLIB_001:77;

then (W .edgeSeq()) . 1 in rng (W .edgeSeq()) by FUNCT_1:3;

then A18: W . (1 + 1) in rng (W .edgeSeq()) by A16, A17, GLIB_001:77;

1 < len W by A8, XXREAL_0:2;

then W . (1 + 1) Joins W . 1,W . (1 + 2),G by A15, GLIB_001:def 3;

hence ( not m = 3 or not n = len W ) by A5, A10, A18, GLIB_000:14; :: thesis: verum

ex m, n being odd Nat st

( m + 2 < n & n <= len W & W . m <> W . n & ex e being object st e Joins W . m,W . n,G & ( W is Cycle-like implies ( ( not m = 1 or not n = len W ) & ( not m = 1 or not n = (len W) - 2 ) & ( not m = 3 or not n = len W ) ) ) )

let W be Walk of G; :: thesis: ( W is chordal implies ex m, n being odd Nat st

( m + 2 < n & n <= len W & W . m <> W . n & ex e being object st e Joins W . m,W . n,G & ( W is Cycle-like implies ( ( not m = 1 or not n = len W ) & ( not m = 1 or not n = (len W) - 2 ) & ( not m = 3 or not n = len W ) ) ) ) )

given m, n being odd Nat such that A1: m + 2 < n and

A2: n <= len W and

A3: W . m <> W . n and

A4: ex e being object st e Joins W . m,W . n,G and

A5: for f being object st f in W .edges() holds

not f Joins W . m,W . n,G ; :: according to CHORD:def 10 :: thesis: ex m, n being odd Nat st

( m + 2 < n & n <= len W & W . m <> W . n & ex e being object st e Joins W . m,W . n,G & ( W is Cycle-like implies ( ( not m = 1 or not n = len W ) & ( not m = 1 or not n = (len W) - 2 ) & ( not m = 3 or not n = len W ) ) ) )

take m ; :: thesis: ex n being odd Nat st

( m + 2 < n & n <= len W & W . m <> W . n & ex e being object st e Joins W . m,W . n,G & ( W is Cycle-like implies ( ( not m = 1 or not n = len W ) & ( not m = 1 or not n = (len W) - 2 ) & ( not m = 3 or not n = len W ) ) ) )

take n ; :: thesis: ( m + 2 < n & n <= len W & W . m <> W . n & ex e being object st e Joins W . m,W . n,G & ( W is Cycle-like implies ( ( not m = 1 or not n = len W ) & ( not m = 1 or not n = (len W) - 2 ) & ( not m = 3 or not n = len W ) ) ) )

thus m + 2 < n by A1; :: thesis: ( n <= len W & W . m <> W . n & ex e being object st e Joins W . m,W . n,G & ( W is Cycle-like implies ( ( not m = 1 or not n = len W ) & ( not m = 1 or not n = (len W) - 2 ) & ( not m = 3 or not n = len W ) ) ) )

thus n <= len W by A2; :: thesis: ( W . m <> W . n & ex e being object st e Joins W . m,W . n,G & ( W is Cycle-like implies ( ( not m = 1 or not n = len W ) & ( not m = 1 or not n = (len W) - 2 ) & ( not m = 3 or not n = len W ) ) ) )

thus W . m <> W . n by A3; :: thesis: ( ex e being object st e Joins W . m,W . n,G & ( W is Cycle-like implies ( ( not m = 1 or not n = len W ) & ( not m = 1 or not n = (len W) - 2 ) & ( not m = 3 or not n = len W ) ) ) )

thus ex e being object st e Joins W . m,W . n,G by A4; :: thesis: ( W is Cycle-like implies ( ( not m = 1 or not n = len W ) & ( not m = 1 or not n = (len W) - 2 ) & ( not m = 3 or not n = len W ) ) )

A6: W .last() = W . (len W) ;

assume A7: W is Cycle-like ; :: thesis: ( ( not m = 1 or not n = len W ) & ( not m = 1 or not n = (len W) - 2 ) & ( not m = 3 or not n = len W ) )

then A8: 3 <= len W by GLIB_001:125;

then reconsider lW2 = (len W) - (2 * 1) as odd Element of NAT by INT_1:5, XXREAL_0:2;

A9: W .first() = W . 1 ;

then A10: W . 1 = W . (len W) by A7, A6, GLIB_001:def 24;

reconsider lW2 = lW2 as odd Nat ;

reconsider le = lW2 + 1 as even Nat ;

A11: 1 <= le by NAT_1:12;

A12: lW2 < len W by XREAL_1:44;

then A13: le <= len W by NAT_1:13;

then le div 2 in dom (W .edgeSeq()) by A11, GLIB_001:77;

then (W .edgeSeq()) . (le div 2) in rng (W .edgeSeq()) by FUNCT_1:3;

then A14: W . (((len W) - 2) + 1) in W .edges() by A11, A13, GLIB_001:77;

thus ( not m = 1 or not n = len W ) by A3, A7, A9, A6, GLIB_001:def 24; :: thesis: ( ( not m = 1 or not n = (len W) - 2 ) & ( not m = 3 or not n = len W ) )

W . (lW2 + 1) Joins W . lW2,W . (lW2 + 2),G by A12, GLIB_001:def 3;

hence ( not m = 1 or not n = (len W) - 2 ) by A5, A10, A14, GLIB_000:14; :: thesis: ( not m = 3 or not n = len W )

A15: (2 * 0) + 1 is odd Nat ;

A16: (2 * 1) div 2 = 1 by NAT_D:18;

A17: 1 + 1 <= len W by A8, XXREAL_0:2;

then 1 in dom (W .edgeSeq()) by A16, GLIB_001:77;

then (W .edgeSeq()) . 1 in rng (W .edgeSeq()) by FUNCT_1:3;

then A18: W . (1 + 1) in rng (W .edgeSeq()) by A16, A17, GLIB_001:77;

1 < len W by A8, XXREAL_0:2;

then W . (1 + 1) Joins W . 1,W . (1 + 2),G by A15, GLIB_001:def 3;

hence ( not m = 3 or not n = len W ) by A5, A10, A18, GLIB_000:14; :: thesis: verum