theorem Th10: :: MSSCYC_1:11

for G being non void Graph
for oc being non empty directed Chain of G
for n being Nat st 1 <= n & n <= len oc holds
( (vertex-seq oc) . n = the Source of G . (oc . n) & (vertex-seq oc) . (n + 1) = the Target of G . (oc . n) )