theorem Th37: :: CHAIN_1:40

for d being non zero Nat
for l, r being Element of REAL d
for G being Grating of d holds
( cell (l,r) in cells (d,G) iff ( ( for i being Element of Seg d holds [(l . i),(r . i)] is Gap of G . i ) & ( for i being Element of Seg d holds l . i < r . i or for i being Element of Seg d holds r . i < l . i ) ) )