for d9 being Nat
for G being Grating of d9 + 1
for C being Chain of (d9 + 1),G holds del (C `) = del C