theorem Th31: :: GLIB_006:27

for G being _Graph
for W being Walk of G
for n being odd Element of NAT st n + 2 <= len W holds
G .walkOf ((W . n),(W . (n + 1)),(W . (n + 2))) is_odd_substring_of W, 0