theorem Th32: :: CHAIN_1:35

for k being Nat
for d being non zero Nat
for l, r being Element of REAL d
for G being Grating of d st k <= d & cell (l,r) in cells (k,G) holds
for i being Element of Seg d holds
( l . i in G . i & r . i in G . i )