for G being _Graph
for W being Walk of G st W is minlength holds
W is chordless by Th39;