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

( cell (l,r) c= cell (l9,r9) iff ex i being Element of Seg d st

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

let l, r, l9, r9 be Element of REAL d; :: thesis: ( ( for i being Element of Seg d holds l . i <= r . i ) & ( for i being Element of Seg d holds r9 . i < l9 . i ) implies ( cell (l,r) c= cell (l9,r9) iff ex i being Element of Seg d st

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

assume A1: for i being Element of Seg d holds l . i <= r . i ; :: thesis: ( ex i being Element of Seg d st not r9 . i < l9 . i or ( cell (l,r) c= cell (l9,r9) iff ex i being Element of Seg d st

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

assume A2: for i being Element of Seg d holds r9 . i < l9 . i ; :: thesis: ( cell (l,r) c= cell (l9,r9) iff ex i being Element of Seg d st

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

thus ( cell (l,r) c= cell (l9,r9) implies ex i being Element of Seg d st

( r . i <= r9 . i or l9 . i <= l . i ) ) :: thesis: ( ex i being Element of Seg d st

( r . i <= r9 . i or l9 . i <= l . i ) implies 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 A14: x in cell (l,r) ; :: thesis: x in cell (l9,r9)

then reconsider x = x as Element of REAL d ;

A15: l . i0 <= x . i0 by A1, A14, Th21;

A16: x . i0 <= r . i0 by A1, A14, Th21;

ex i being Element of Seg d st

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

( cell (l,r) c= cell (l9,r9) iff ex i being Element of Seg d st

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

let l, r, l9, r9 be Element of REAL d; :: thesis: ( ( for i being Element of Seg d holds l . i <= r . i ) & ( for i being Element of Seg d holds r9 . i < l9 . i ) implies ( cell (l,r) c= cell (l9,r9) iff ex i being Element of Seg d st

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

assume A1: for i being Element of Seg d holds l . i <= r . i ; :: thesis: ( ex i being Element of Seg d st not r9 . i < l9 . i or ( cell (l,r) c= cell (l9,r9) iff ex i being Element of Seg d st

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

assume A2: for i being Element of Seg d holds r9 . i < l9 . i ; :: thesis: ( cell (l,r) c= cell (l9,r9) iff ex i being Element of Seg d st

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

thus ( cell (l,r) c= cell (l9,r9) implies ex i being Element of Seg d st

( r . i <= r9 . i or l9 . i <= l . i ) ) :: thesis: ( ex i being Element of Seg d st

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

proof

given i0 being Element of Seg d such that A13:
( r . i0 <= r9 . i0 or l9 . i0 <= l . i0 )
; :: thesis: cell (l,r) c= cell (l9,r9)
assume A3:
cell (l,r) c= cell (l9,r9)
; :: thesis: ex i being Element of Seg d st

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

assume A4: for i being Element of Seg d holds

( r9 . i < r . i & l . i < l9 . i ) ; :: thesis: contradiction

defpred S_{1}[ Element of Seg d, Element of REAL ] means ( l . $1 <= $2 & $2 <= r . $1 & r9 . $1 < $2 & $2 < l9 . $1 );

A5: for i being Element of Seg d ex xi being Element of REAL st S_{1}[i,xi]

A11: for i being Element of Seg d holds S_{1}[i,x . i]
from FUNCT_2:sch 3(A5);

reconsider x = x as Element of REAL d by Def3;

A12: x in cell (l,r) by A11;

set i0 = the Element of Seg d;

r9 . the Element of Seg d < l9 . the Element of Seg d by A2;

then ex i being Element of Seg d st

( r9 . i < l9 . i & ( x . i <= r9 . i or l9 . i <= x . i ) ) by A3, A12, Th22;

hence contradiction by A11; :: thesis: verum

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

assume A4: for i being Element of Seg d holds

( r9 . i < r . i & l . i < l9 . i ) ; :: thesis: contradiction

defpred S

A5: for i being Element of Seg d ex xi being Element of REAL st S

proof

consider x being Function of (Seg d),REAL such that
let i be Element of Seg d; :: thesis: ex xi being Element of REAL st S_{1}[i,xi]

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

end;

suppose A6:
( l . i <= r9 . i & l9 . i <= r . i )
; :: thesis: ex xi being Element of REAL st S_{1}[i,xi]

r9 . i < l9 . i
by A2;

then consider xi being Element of REAL such that

A7: r9 . i < xi and

A8: xi < l9 . i by Th1;

take xi ; :: thesis: S_{1}[i,xi]

thus S_{1}[i,xi]
by A6, A7, A8, XXREAL_0:2; :: thesis: verum

end;then consider xi being Element of REAL such that

A7: r9 . i < xi and

A8: xi < l9 . i by Th1;

take xi ; :: thesis: S

thus S

suppose A9:
( r9 . i < l . i & l9 . i <= r . i )
; :: thesis: ex xi being Element of REAL st S_{1}[i,xi]

reconsider li = l . i as Element of REAL by XREAL_0:def 1;

take li ; :: thesis: S_{1}[i,li]

thus S_{1}[i,li]
by A1, A4, A9; :: thesis: verum

end;take li ; :: thesis: S

thus S

suppose A10:
r . i < l9 . i
; :: thesis: ex xi being Element of REAL st S_{1}[i,xi]

reconsider ri = r . i as Element of REAL by XREAL_0:def 1;

take ri ; :: thesis: S_{1}[i,ri]

thus S_{1}[i,ri]
by A1, A4, A10; :: thesis: verum

end;take ri ; :: thesis: S

thus S

A11: for i being Element of Seg d holds S

reconsider x = x as Element of REAL d by Def3;

A12: x in cell (l,r) by A11;

set i0 = the Element of Seg d;

r9 . the Element of Seg d < l9 . the Element of Seg d by A2;

then ex i being Element of Seg d st

( r9 . i < l9 . i & ( x . i <= r9 . i or l9 . i <= x . i ) ) by A3, A12, Th22;

hence contradiction by A11; :: thesis: verum

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

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

then reconsider x = x as Element of REAL d ;

A15: l . i0 <= x . i0 by A1, A14, Th21;

A16: x . i0 <= r . i0 by A1, A14, Th21;

ex i being Element of Seg d st

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

proof

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

thus ( r9 . i0 < l9 . i0 & ( x . i0 <= r9 . i0 or l9 . i0 <= x . i0 ) ) by A2, A13, A15, A16, XXREAL_0:2; :: thesis: verum

end;thus ( r9 . i0 < l9 . i0 & ( x . i0 <= r9 . i0 or l9 . i0 <= x . i0 ) ) by A2, A13, A15, A16, XXREAL_0:2; :: thesis: verum