theorem :: GLIB_001:58

for G being _Graph
for W being Walk of G
for m being Element of NAT st W .first() = W . m holds
W .remove (1,m) = W .cut (m,(len W)) by Lm32;