theorem Th26: :: CHAIN_1:29

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