for G being _Graph
for W1, W2 being Walk of G st W1 is Subwalk of W2 holds
len W1 <= len W2 by Lm72;