theorem :: GLIB_001:165

for G being _Graph
for W1, W2 being Walk of G st W1 is Subwalk of W2 holds
for m being even Element of NAT st 1 <= m & m <= len W1 holds
ex n being even Element of NAT st
( m <= n & n <= len W2 & W1 . m = W2 . n )