let d be non zero Nat; :: thesis:
let l, r, l9, r9 be Element of REAL d; :: thesis:
assume A1: for i being Element of Seg d holds l9 . i <= r9 . i ; :: thesis:
thus ( cell (l,r) c= cell (l9,r9) implies for i being Element of Seg d holds
( l9 . i <= l . i & l . i <= r . i & r . i <= r9 . i ) ) :: thesis:

assume A2: cell (l,r) c= cell (l9,r9) ; :: thesis:
let i0 be Element of Seg d; :: thesis:

defpred S₁[ Element of Seg d, Element of REAL ] means ( $2 > l . $1 & $2 > r9 . $1 );
A4: for i being Element of Seg d ex xi being Element of REAL st S₁[i,xi] by Th2;
consider x being Function of (Seg d),REAL such that
A5: for i being Element of Seg d holds S₁[i,x . i] from FUNCT_2:sch 3(A4);
reconsider x = x as Element of REAL d by Def3;
ex i being Element of Seg d st
( r . i < l . i & ( x . i <= r . i or l . i <= x . i ) )

take i0 ; :: thesis:
thus ( r . i0 < l . i0 & ( x . i0 <= r . i0 or l . i0 <= x . i0 ) ) by A3, A5; :: thesis:

end;

then A6: x in cell (l,r) ;
ex i being Element of Seg d st
( x . i < l9 . i or r9 . i < x . i )

take i0 ; :: thesis:
thus ( x . i0 < l9 . i0 or r9 . i0 < x . i0 ) by A5; :: thesis:

end;

hence ( l9 . i0 <= l . i0 & l . i0 <= r . i0 & r . i0 <= r9 . i0 ) by A1, A2, A6, Th21; :: thesis:

end;

A8: l in cell (l,r) by Th23;
r in cell (l,r) by Th23;
hence ( l9 . i0 <= l . i0 & l . i0 <= r . i0 & r . i0 <= r9 . i0 ) by A1, A2, A7, A8, Th21; :: thesis:

end;

assume A9: for i being Element of Seg d holds
( l9 . i <= l . i & l . i <= r . i & r . i <= r9 . i ) ; :: thesis:
let x be object ; :: according to TARSKI:def 3 :: thesis:
assume A10: x in cell (l,r) ; :: thesis:
then reconsider x = x as Element of REAL d ;

end;

hence x in cell (l9,r9) ; :: thesis: