for G being _Graph
for W1, W2 being Walk of G st W1 is Subwalk of W2 holds
( W1 .first() = W2 .first() & W1 .last() = W2 .last() )