theorem Th9: :: GRAPH_4:9

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