theorem Th87: :: GLIB_001:89
for G being _Graph
for W being Walk of G
for n being odd Element of NAT st n <= len W holds
W .vertexAt n in W .vertices()