theorem Th49: :: CHAIN_1:52
for k being Nat
for d being non zero Nat
for G being Grating of d st k + 1 > d holds
for C being Chain of (k + 1),G holds del C = 0_ (k,G)