for G being _Graph
for W1, W2 being Walk of G st W2 is_odd_substring_of W1, 0 holds
( W1 . (W1 .findFirstVertex W2) = W2 .first() & W1 . (W1 .findLastVertex W2) = W2 .last() )