:: deftheorem Def3 defines Walk GLIB_001:def 3 :
for G being _Graph
for b₂ being FinSequence of (the_Vertices_of G) \/ (the_Edges_of G) holds
( b₂ is Walk of G iff ( len b₂ is odd & b₂ . 1 in the_Vertices_of G & ( for n being odd Element of NAT st n < len b₂ holds
b₂ . (n + 1) Joins b₂ . n,b₂ . (n + 2),G ) ) );