theorem Th38: :: CHAIN_1:41

for d9 being Nat
for d being non zero Nat
for G being Grating of d st d = d9 + 1 holds
for A being Subset of (REAL d) holds
( A in cells (d9,G) iff ex l, r being Element of REAL d ex i0 being Element of Seg d st
( A = cell (l,r) & l . i0 = r . i0 & l . i0 in G . i0 & ( for i being Element of Seg d st i <> i0 holds
( l . i < r . i & [(l . i),(r . i)] is Gap of G . i ) ) ) )