theorem :: GLIB_001:99

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