theorem Th83: :: CHORD:84

for G being _Graph
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 ) ) ) )