theorem :: GLIB_001:50
for G being _Graph
for W being Walk of G
for x, y being set
for n, m being Element of NAT st W is_Walk_from x,y holds
W .remove (m,n) is_Walk_from x,y by Lm25;