theorem Th98: :: GLIB_001:100

for G being _Graph
for W being Walk of G
for e being set holds
( e in W .edges() iff ex n being odd Element of NAT st
( n < len W & W . (n + 1) = e ) )