:: deftheorem defines bounds CHAIN_1:def 13 :
for d being non zero Nat
for G being Grating of d
for k being Nat
for C being Chain of (k + 1),G
for C9 being Chain of k,G holds
( C9 bounds C iff C9 = del C );