for G being finite Graph
for v being Vertex of G
for c being Chain of G
for vs being FinSequence of the carrier of G st not c is empty & vs is_vertex_seq_of c holds
( v in rng vs iff Degree (v,(rng c)) <> 0 )