theorem Th21: :: CHAIN_1:24

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