for G being _Graph
for W1, W2 being Walk of G st W2 is_odd_substring_of W1, 0 holds
( 1 <= W1 .findFirstVertex W2 & W1 .findFirstVertex W2 <= len W1 & 1 <= W1 .findLastVertex W2 & W1 .findLastVertex W2 <= len W1 ) by Def3, Def4, ABIAN:12;