let G be _Graph; :: thesis: for W1, W2 being Walk of G st W2 is_odd_substring_of W1, 0 holds
W1 .findFirstVertex W2 <= W1 .findLastVertex W2
let W1, W2 be Walk of G; :: thesis: ( W2 is_odd_substring_of W1, 0 implies W1 .findFirstVertex W2 <= W1 .findLastVertex W2 )
assume A1: W2 is_odd_substring_of W1, 0 ; :: thesis: W1 .findFirstVertex W2 <= W1 .findLastVertex W2
then consider k1 being even Nat such that
A2: W1 .findFirstVertex W2 = k1 + 1 and
A3: for n being Nat st 1 <= n & n <= len W2 holds
W1 . (k1 + n) = W2 . n and
A4: for l being even Nat st ( for n being Nat st 1 <= n & n <= len W2 holds
W1 . (l + n) = W2 . n ) holds
k1 <= l by Def3;
consider k2 being even Nat such that
A5: W1 .findLastVertex W2 = k2 + (len W2) and
A6: for n being Nat st 1 <= n & n <= len W2 holds
W1 . (k2 + n) = W2 . n and
A7: for l being even Nat st ( for n being Nat st 1 <= n & n <= len W2 holds
W1 . (l + n) = W2 . n ) holds
k2 <= l by A1, Def4;
k1 = k2

proof

A9: k2 <= k1 by A3, A7;
k1 <= k2 by A4, A6;
hence k1 = k2 by A9, XXREAL_0:1; :: thesis: verum

end;

hence W1 .findFirstVertex W2 <= W1 .findLastVertex W2 by A2, A5, ABIAN:12, XREAL_1:6; :: thesis: verum