for G being _Graph
for W being Walk of G st W is minlength holds
for m, n being odd Nat st m <= n & n <= len W holds
W .cut (m,n) is minlength