theorem Th31: :: GRAPH_2:31

for G being Graph
for vs being FinSequence of the carrier of G
for c being Chain of G st c <> {} & vs is_vertex_seq_of c holds
G -VSet (rng c) = rng vs