:: deftheorem defines del CHAIN_1:def 12 :
for d being non zero Nat
for G being Grating of d
for k being Nat
for C being Chain of (k + 1),G holds del C = { A where A is Cell of k,G : ( k + 1 <= d & card ((star A) /\ C) is odd ) } ;