theorem Th35: :: GRAPH_2:35

for G being Graph
for vs being FinSequence of the carrier of G
for c being Chain of G st c alternates_vertices_in G & vs is_vertex_seq_of c holds
for k being Nat st k in dom c holds
vs . k <> vs . (k + 1)