theorem Th9: :: GLIB_001:10

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