:: deftheorem defines 0_ CHAIN_1:def 8 :
for d being non zero Nat
for G being Grating of d
for k being Nat holds 0_ (k,G) = {} ;