:: deftheorem Def10 defines infinite-cell CHAIN_1:def 10 :
for d being non zero Nat
for G being Grating of d
for b₃ being Cell of d,G holds
( b₃ = infinite-cell G iff ex l, r being Element of REAL d st
( b₃ = cell (l,r) & ( for i being Element of Seg d holds
( r . i < l . i & [(l . i),(r . i)] is Gap of G . i ) ) ) );