theorem :: GLIB_001:7

for G being _Graph
for W being Walk of G
for n being odd Element of NAT st n <= len W holds
W . n in the_Vertices_of G by Lm1;