:: deftheorem defines .edges() GLIB_001:def 17 :
for G being _Graph
for W being Walk of G holds W .edges() = rng (W .edgeSeq());