for G being Graph
for vs being FinSequence of the carrier of G
for c being Chain of G st vs is_vertex_seq_of c holds
( ( card the carrier of G = 1 or ( c <> {} & not c alternates_vertices_in G ) ) iff for vs1 being FinSequence of the carrier of G st vs1 is_vertex_seq_of c holds
vs1 = vs )