theorem Th102: :: GLIB_001:104

for G being _Graph
for W being Walk of G
for e being set holds
( e in W .edges() iff ex n being Element of NAT st
( n in dom (W .edgeSeq()) & (W .edgeSeq()) . n = e ) )