for G being Graph
for c being Chain of G ex vs being FinSequence of the carrier of G st vs is_vertex_seq_of c