theorem :: GLIB_001:117

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