theorem Th34: :: CHAIN_1:37

for d being non zero Nat
for G being Grating of d
for A being Subset of (REAL d) holds
( A in cells (0,G) iff ex x being Element of REAL d st
( A = cell (x,x) & ( for i being Element of Seg d holds x . i in G . i ) ) )