theorem :: GLIB_001:60

for G being _Graph
for W being Walk of G
for m, n being odd Element of NAT
for x being Element of NAT st m <= n & n <= len W & W . m = W . n & x in dom (W .remove (m,n)) & not x in Seg m holds
( m <= x & x <= len (W .remove (m,n)) ) by Lm34;