:: deftheorem Def21 defines .rfind GLIB_001:def 21 :
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 .rfind v iff ( b₄ <= len W & W . b₄ = v & ( for n being odd Element of NAT st n <= len W & W . n = v holds
n <= b₄ ) ) ) ) & ( not v in W .vertices() implies ( b₄ = W .rfind v iff b₄ = len W ) ) );