theorem :: GLIB_001:52

for G being _Graph
for W being Walk of G
for m being Element of NAT holds W .remove (m,m) = W by Lm27;