for G being non void Graph
for c being non empty directed Chain of G st c is cyclic holds
for n being Nat ex ch being directed Chain of G st
( len ch = n & ch ^ c is non empty directed Chain of G )