:: deftheorem defines cell CHAIN_1:def 6 :
for d being non zero Nat
for l, r being Element of REAL d holds cell (l,r) = { x where x is Element of REAL d : ( 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 ) ) ) } ;