theorem Th50: :: CHAIN_1:53

for k being Nat
for d being non zero Nat
for G being Grating of d st k + 1 <= d holds
for A being Cell of k,G
for B being Cell of (k + 1),G holds
( A in del {B} iff A c= B )