:: deftheorem defines minlength CHORD:def 2 :
for G being _Graph
for W being Walk of G holds
( W is minlength iff for W2 being Walk of G st W2 is_Walk_from W .first() ,W .last() holds
len W2 >= len W );