theorem :: GLIB_001:9

for G being _Graph
for W being Walk of G
for n being even Element of NAT st n in dom W holds
ex naa1 being odd Element of NAT st
( naa1 = n - 1 & n - 1 in dom W & n + 1 in dom W & W . n Joins W . naa1,W . (n + 1),G ) by Lm2;