theorem :: GLIB_006:29

for G being _Graph
for W being Walk of G
for u, e, v being object st e Joins u,v,G & G .walkOf (u,e,v) is_odd_substring_of W, 0 holds
( e in W .edges() & u in W .vertices() & v in W .vertices() )