theorem Th9: :: MSSCYC_1:10

for G being non void Graph
for oc being non empty directed Chain of G holds len (vertex-seq oc) = (len oc) + 1