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 ;
A9: W .first() = W . 1 ;
then A10: W . 1 = W . (len W) by ;
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 () by ;
then (W .edgeSeq()) . (le div 2) in rng () by FUNCT_1:3;
then A14: W . (((len W) - 2) + 1) in W .edges() by ;
thus ( not m = 1 or not n = len W ) by ; :: 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 ;
hence ( not m = 1 or not n = (len W) - 2 ) by ; :: 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 ;
then 1 in dom () by ;
then (W .edgeSeq()) . 1 in rng () by FUNCT_1:3;
then A18: W . (1 + 1) in rng () by ;
1 < len W by ;
then W . (1 + 1) Joins W . 1,W . (1 + 2),G by ;
hence ( not m = 3 or not n = len W ) by ; :: thesis: verum