for G being Graph
for c being Chain of G
for vs being FinSequence of the carrier of G
for e being set st vs is_vertex_seq_of c & e in rng c holds
( the Target of G . e in rng vs & the Source of G . e in rng vs )