theorem Th25: :: CHAIN_1:28

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 l9 . i <= r9 . i ) holds
( cell (l,r) c= cell (l9,r9) iff for i being Element of Seg d holds
( l9 . i <= l . i & l . i <= r . i & r . i <= r9 . i ) )