theorem Th20: :: CHAIN_1:23

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