:: deftheorem Def19 defines .find GLIB_001:def 19 :
for G being _Graph
for W being Walk of G
for v being set
for b₄ being odd Element of NAT holds
( ( v in W .vertices() implies ( b₄ = W .find v iff ( b₄ <= len W & W . b₄ = v & ( for n being odd Nat st n <= len W & W . n = v holds
b₄ <= n ) ) ) ) & ( not v in W .vertices() implies ( b₄ = W .find v iff b₄ = len W ) ) );