theorem Th60: :: CHAIN_1:63

for k being Nat
for d being non zero Nat
for G being Grating of d
for C being Chain of ((k + 1) + 1),G holds del (del C) = 0_ (k,G)