:: deftheorem defines del CHAIN_1:def 15 :
for d being non zero Nat
for G being Grating of d
for k being Nat
for C being Cycle of k + 1,G holds del C = 0_ (k,G);