theorem Th45: :: CHAIN_1:48

for d being non zero Nat
for l, r being Element of REAL d
for G being Grating of d st cell (l,r) is Cell of d,G holds
( cell (l,r) = infinite-cell G iff for i being Element of Seg d holds r . i < l . i )