theorem Th16: :: MSSCYC_1:17

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