theorem :: GLIB_001:49

for G being _Graph
for W being Walk of G
for m, n being odd Element of NAT st m <= n & n <= len W & W . m = W . n holds
(len (W .remove (m,n))) + n = (len W) + m by Lm24;