theorem :: GLIB_001:44

for G being _Graph
for W1, W2 being Walk of G
for m, n being odd Element of NAT st m <= n & n <= len W1 & W1 .last() = W2 .first() holds
(W1 .append W2) .cut (m,n) = W1 .cut (m,n) by Lm21;