theorem Th22: :: CHAIN_1:25

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