:: deftheorem Def1 defines VertexSeq GLIB_001:def 1 :
for G being _Graph
for b₂ being FinSequence of the_Vertices_of G holds
( b₂ is VertexSeq of G iff for n being Element of NAT st 1 <= n & n < len b₂ holds
ex e being set st e Joins b₂ . n,b₂ . (n + 1),G );