:: deftheorem defines del CHAIN_1:def 17 :
for d being non zero Nat
for G being Grating of d
for k being Nat
for b₄ being Homomorphism of (Chains ((k + 1),G)),(Chains (k,G)) holds
( b₄ = del (k,G) iff for A being Element of (Chains ((k + 1),G))
for A9 being Chain of (k + 1),G st A = A9 holds
b₄ . A = del A9 );