for k being Nat
for d being non zero Nat
for G being Grating of d
for A being Cell of k,G
for C being Chain of (k + 1),G holds
( A in del C iff ( k + 1 <= d & card ((star A) /\ C) is odd ) )