for G being _Graph
for W1, W2 being Walk of G st W1 .last() = W2 .first() holds
( len W1 <= len (W1 .append W2) & len W2 <= len (W1 .append W2) ) by Lm10;