:: deftheorem Def14 defines Cycle CHAIN_1:def 14 :
for d being non zero Nat
for G being Grating of d
for k being Nat
for b₄ being Chain of k,G holds
( b₄ is Cycle of k,G iff ( ( k = 0 & card b₄ is even ) or ex k9 being Nat st
( k = k9 + 1 & ex C being Chain of (k9 + 1),G st
( C = b₄ & del C = 0_ (k9,G) ) ) ) );