let G be _Graph; :: thesis: for W being Walk of G st W is minlength holds
not W is chordal
let W be Walk of G; :: thesis: ( W is minlength implies not W is chordal )
assume A1: W is minlength ; :: thesis: not W is chordal
assume W is chordal ; :: thesis: contradiction
then ex m, n being odd Nat st
( m + 2 < n & n <= len W & W . m <> W . n & ex e being set 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 ) ) ) ) by Th84;
hence contradiction by A1, Th40; :: thesis: verum