:: deftheorem Def25 defines directed GLIB_001:def 25 :
for G being _Graph
for W being Walk of G holds
( W is directed iff for n being odd Element of NAT st n < len W holds
(the_Source_of G) . (W . (n + 1)) = W . n );