theorem Th10: :: GLIB_001:11

for G being _Graph
for W being Walk of G
for n being odd Element of NAT st 1 < n & n <= len W holds
W . (n - 1) in (W .vertexAt n) .edgesInOut()