theorem :: GLIB_001:51

for G being _Graph
for W being Walk of G
for n, m being Element of NAT holds len (W .remove (m,n)) <= len W by Lm26;