theorem :: GLIB_001:158

for G being _Graph
for W being Walk of G holds W is Subwalk of W by Lm70;