theorem Th4: :: GRAPH_4:4

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