theorem :: GLIB_001:131

for G being _Graph
for W being Walk of G
for m, n being odd Element of NAT st m <= n & n <= len W holds
( W .cut (m,n) is trivial iff m = n )