for G being _Graph
for W being Walk of G holds W is Subwalk of W by Lm70;