:: deftheorem Def22 defines .rfind GLIB_001:def 22 :
for G being _Graph
for W being Walk of G
for n being Element of NAT
for b₄ being odd Element of NAT holds
( ( n is odd & n <= len W implies ( b₄ = W .rfind n iff ( b₄ <= len W & W . b₄ = W . n & ( for k being odd Element of NAT st k <= len W & W . k = W . n holds
k <= b₄ ) ) ) ) & ( ( not n is odd or not n <= len W ) implies ( b₄ = W .rfind n iff b₄ = len W ) ) );