theorem :: GLIB_001:36

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
( (len (W .cut (m,n))) + m = n + 1 & ( for i being Element of NAT st i < len (W .cut (m,n)) holds
( (W .cut (m,n)) . (i + 1) = W . (m + i) & m + i in dom W ) ) ) by Lm15;