theorem :: GLIB_001:37

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)) .first() = W . m & (W .cut (m,n)) .last() = W . n & W .cut (m,n) is_Walk_from W . m,W . n ) by Lm16;