theorem :: GLIB_001:109

for G being _Graph
for W being Walk of G holds W .edges() c= G .edgesBetween (W .vertices())