theorem Th113: :: GLIB_001:115

for G being _Graph
for W being Walk of G
for n being odd Element of NAT st n <= len W holds
( W .find (W . n) <= n & W .rfind (W . n) >= n )