:: deftheorem Def14 defines .vertexSeq() GLIB_001:def 14 :
for G being _Graph
for W being Walk of G
for b₃ being VertexSeq of G holds
( b₃ = W .vertexSeq() iff ( (len W) + 1 = 2 * (len b₃) & ( for n being Nat st 1 <= n & n <= len b₃ holds
b₃ . n = W . ((2 * n) - 1) ) ) );