:: deftheorem Def4 defines .findLastVertex GLIB_006:def 4 :
for G being _Graph
for W1, W2 being Walk of G
for b₄ being odd Element of NAT holds
( ( W2 is_odd_substring_of W1, 0 implies ( b₄ = W1 .findLastVertex W2 iff ( b₄ <= len W1 & ex k being even Nat st
( b₄ = k + (len W2) & ( for n being Nat st 1 <= n & n <= len W2 holds
W1 . (k + n) = W2 . n ) & ( for l being even Nat st ( for n being Nat st 1 <= n & n <= len W2 holds
W1 . (l + n) = W2 . n ) holds
k <= l ) ) ) ) ) & ( not W2 is_odd_substring_of W1, 0 implies ( b₄ = W1 .findLastVertex W2 iff b₄ = len W1 ) ) );