theorem :: CHAIN_1:36

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) & not for i being Element of Seg d holds l . i <= r . i holds
for i being Element of Seg d holds r . i < l . i by Th31;