theorem :: GLIB_001:45

for G being _Graph
for W being Walk of G
for m being odd Element of NAT st m <= len W holds
len (W .cut (1,m)) = m by Lm22;