theorem :: GRAPH_3:14

for G being Graph
for c being Chain of G
for vs being FinSequence of the carrier of G st vs is_vertex_seq_of c holds
for n being Element of NAT holds
( not n in dom c or ( vs . n = the Target of G . (c . n) & vs . (n + 1) = the Source of G . (c . n) ) or ( vs . n = the Source of G . (c . n) & vs . (n + 1) = the Target of G . (c . n) ) )