:: deftheorem defines vertex-seq GRAPH_2:def 8 :
for G being Graph
for c being Chain of G st ( card the carrier of G = 1 or ( c <> {} & not c alternates_vertices_in G ) ) holds
for b₃ being FinSequence of the carrier of G holds
( b₃ = vertex-seq c iff b₃ is_vertex_seq_of c );