let d be non zero Nat; :: thesis: 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 ) )

let l, r, l9, r9 be Element of REAL d; :: thesis: ( ( for i being Element of Seg d holds l9 . i <= r9 . i ) implies ( 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 ) ) )

assume A1: for i being Element of Seg d holds l9 . i <= r9 . i ; :: thesis: ( 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 ) )

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: ( ( for i being Element of Seg d holds

( l9 . i <= l . i & l . i <= r . i & r . i <= r9 . i ) ) implies cell (l,r) c= cell (l9,r9) )

( l9 . i <= l . i & l . i <= r . i & r . i <= r9 . i ) ; :: thesis: cell (l,r) c= cell (l9,r9)

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in cell (l,r) or x in cell (l9,r9) )

assume A10: x in cell (l,r) ; :: thesis: x in cell (l9,r9)

then reconsider x = x as Element of REAL d ;

( 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 ) )

let l, r, l9, r9 be Element of REAL d; :: thesis: ( ( for i being Element of Seg d holds l9 . i <= r9 . i ) implies ( 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 ) ) )

assume A1: for i being Element of Seg d holds l9 . i <= r9 . i ; :: thesis: ( 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 ) )

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: ( ( for i being Element of Seg d holds

( l9 . i <= l . i & l . i <= r . i & r . i <= r9 . i ) ) implies cell (l,r) c= cell (l9,r9) )

proof

assume A9:
for i being Element of Seg d holds
assume A2:
cell (l,r) c= cell (l9,r9)
; :: thesis: for i being Element of Seg d holds

( l9 . i <= l . i & l . i <= r . i & r . i <= r9 . i )

let i0 be Element of Seg d; :: thesis: ( l9 . i0 <= l . i0 & l . i0 <= r . i0 & r . i0 <= r9 . i0 )

end;( l9 . i <= l . i & l . i <= r . i & r . i <= r9 . i )

let i0 be Element of Seg d; :: thesis: ( l9 . i0 <= l . i0 & l . i0 <= r . i0 & r . i0 <= r9 . i0 )

per cases
( r . i0 < l . i0 or l . i0 <= r . i0 )
;

end;

suppose A3:
r . i0 < l . i0
; :: thesis: ( l9 . i0 <= l . i0 & l . i0 <= r . i0 & r . i0 <= r9 . i0 )

defpred S_{1}[ 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_{1}[i,xi]
by Th2;

consider x being Function of (Seg d),REAL such that

A5: for i being Element of Seg d holds S_{1}[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 ) )

ex i being Element of Seg d st

( x . i < l9 . i or r9 . i < x . i )

end;A4: for i being Element of Seg d ex xi being Element of REAL st S

consider x being Function of (Seg d),REAL such that

A5: for i being Element of Seg d holds S

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 ) )

proof

then A6:
x in cell (l,r)
;
take
i0
; :: thesis: ( r . i0 < l . i0 & ( x . i0 <= r . i0 or l . i0 <= x . i0 ) )

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

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

ex i being Element of Seg d st

( x . i < l9 . i or r9 . i < x . i )

proof

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

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

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

( l9 . i <= l . i & l . i <= r . i & r . i <= r9 . i ) ; :: thesis: cell (l,r) c= cell (l9,r9)

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in cell (l,r) or x in cell (l9,r9) )

assume A10: x in cell (l,r) ; :: thesis: x in cell (l9,r9)

then reconsider x = x as Element of REAL d ;

now :: thesis: for i being Element of Seg d holds

( l9 . i <= x . i & x . i <= r9 . i & l9 . i <= r9 . i )

hence
x in cell (l9,r9)
; :: thesis: verum( l9 . i <= x . i & x . i <= r9 . i & l9 . i <= r9 . i )

let i be Element of Seg d; :: thesis: ( l9 . i <= x . i & x . i <= r9 . i & l9 . i <= r9 . i )

A11: l9 . i <= l . i by A9;

A12: l . i <= x . i by A9, A10, Th21;

A13: x . i <= r . i by A9, A10, Th21;

r . i <= r9 . i by A9;

hence ( l9 . i <= x . i & x . i <= r9 . i ) by A11, A12, A13, XXREAL_0:2; :: thesis: l9 . i <= r9 . i

hence l9 . i <= r9 . i by XXREAL_0:2; :: thesis: verum

end;A11: l9 . i <= l . i by A9;

A12: l . i <= x . i by A9, A10, Th21;

A13: x . i <= r . i by A9, A10, Th21;

r . i <= r9 . i by A9;

hence ( l9 . i <= x . i & x . i <= r9 . i ) by A11, A12, A13, XXREAL_0:2; :: thesis: l9 . i <= r9 . i

hence l9 . i <= r9 . i by XXREAL_0:2; :: thesis: verum