theorem :: GLIB_001:146

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