theorem Th55: :: GLIB_001:57

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