theorem :: GLIB_001:153

for G being _Graph
for W being Walk of G st ( for n being odd Element of NAT st n <= len W holds
W .rfind n = n ) holds
W is Path-like by Lm67;