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

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

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

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

( r . i <= r9 . i & r9 . i < l9 . i & l9 . i <= l . i ) ) :: thesis: ( ( for i being Element of Seg d holds

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

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

then reconsider x = x as Element of REAL d ;

set i0 = the Element of Seg d;

A37: r . the Element of Seg d <= r9 . the Element of Seg d by A35;

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

then A38: r . the Element of Seg d < l9 . the Element of Seg d by A37, XXREAL_0:2;

l9 . the Element of Seg d <= l . the Element of Seg d by A35;

then r . the Element of Seg d < l . the Element of Seg d by A38, XXREAL_0:2;

then ( x . the Element of Seg d < l . the Element of Seg d or r . the Element of Seg d < x . the Element of Seg d ) by XXREAL_0:2;

then consider i being Element of Seg d such that

r . i < l . i and

A39: ( x . i <= r . i or l . i <= x . i ) by A36, Th20;

A40: r . i <= r9 . i by A35;

A41: l9 . i <= l . i by A35;

A42: r9 . i < l9 . i by A35;

( x . i <= r9 . i or l9 . i <= x . i ) by A39, A40, A41, XXREAL_0:2;

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

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

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

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

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

( r . i <= r9 . i & r9 . i < l9 . i & l9 . i <= l . i ) ) :: thesis: ( ( for i being Element of Seg d holds

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

proof

assume A35:
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

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

A3: for i being Element of Seg d holds r9 . i < l9 . i

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

A3: for i being Element of Seg d holds r9 . i < l9 . i

proof

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

assume A4: l9 . i0 <= r9 . i0 ; :: thesis: contradiction

defpred S_{1}[ Element of Seg d, Element of REAL ] means ( ( $1 = i0 implies ( l . $1 < $2 & r9 . $1 < $2 ) ) & ( r9 . $1 < l9 . $1 implies ( 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]

A8: 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;

A9: r . i0 < l . i0 by A1;

( x . i0 <= r . i0 or l . i0 <= x . i0 ) by A8;

then A10: x in cell (l,r) by A9;

end;assume A4: l9 . i0 <= r9 . i0 ; :: 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
( ( i = i0 & r9 . i < l9 . i ) or i <> i0 or l9 . i <= r9 . i )
;

end;

A8: for i being Element of Seg d holds S

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

A9: r . i0 < l . i0 by A1;

( x . i0 <= r . i0 or l . i0 <= x . i0 ) by A8;

then A10: x in cell (l,r) by A9;

per cases
( for i being Element of Seg d holds

( l9 . i <= x . i & x . i <= r9 . i ) or ex i being Element of Seg d st

( r9 . i < l9 . i & ( x . i <= r9 . i or l9 . i <= x . i ) ) ) by A2, A10, Th20;

end;

( l9 . i <= x . i & x . i <= r9 . i ) or ex i being Element of Seg d st

( r9 . i < l9 . i & ( x . i <= r9 . i or l9 . i <= x . i ) ) ) by A2, A10, Th20;

suppose
for i being Element of Seg d holds

( l9 . i <= x . i & x . i <= r9 . i ) ; :: thesis: contradiction

end;

( l9 . i <= x . i & x . i <= r9 . i ) ; :: thesis: contradiction

end;

hereby :: thesis: ( r9 . i0 < l9 . i0 & l9 . i0 <= l . i0 )

thus
r9 . i0 < l9 . i0
by A3; :: thesis: l9 . i0 <= l . i0assume A11:
r9 . i0 < r . i0
; :: thesis: contradiction

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

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

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

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

A21: r . i0 < l . i0 by A1;

( x . i0 <= r . i0 or l . i0 <= x . i0 ) by A20;

then A22: x in cell (l,r) by A21;

( not l9 . i0 <= x . i0 or not x . i0 <= r9 . i0 ) by A3, XXREAL_0:2;

then ex i being Element of Seg d st

( r9 . i < l9 . i & ( x . i <= r9 . i or l9 . i <= x . i ) ) by A2, A22, Th20;

hence contradiction by A20; :: thesis: verum

end;defpred S

A12: 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
( ( i = i0 & l9 . i <= r . i ) or ( i = i0 & r . i <= l9 . i ) or i <> i0 )
;

end;

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

r9 . i < l9 . i
by A3;

then consider xi being Element of REAL such that

A14: r9 . i < xi and

A15: xi < l9 . i by Th1;

xi < r . i by A13, A15, XXREAL_0:2;

hence ex xi being Element of REAL st S_{1}[i,xi]
by A14, A15; :: thesis: verum

end;then consider xi being Element of REAL such that

A14: r9 . i < xi and

A15: xi < l9 . i by Th1;

xi < r . i by A13, A15, XXREAL_0:2;

hence ex xi being Element of REAL st S

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

then consider xi being Element of REAL such that

A17: r9 . i < xi and

A18: xi < r . i by A11, Th1;

xi < l9 . i by A16, A18, XXREAL_0:2;

hence ex xi being Element of REAL st S_{1}[i,xi]
by A17, A18; :: thesis: verum

end;A17: r9 . i < xi and

A18: xi < r . i by A11, Th1;

xi < l9 . i by A16, A18, XXREAL_0:2;

hence ex xi being Element of REAL st S

A20: for i being Element of Seg d holds S

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

A21: r . i0 < l . i0 by A1;

( x . i0 <= r . i0 or l . i0 <= x . i0 ) by A20;

then A22: x in cell (l,r) by A21;

( not l9 . i0 <= x . i0 or not x . i0 <= r9 . i0 ) by A3, XXREAL_0:2;

then ex i being Element of Seg d st

( r9 . i < l9 . i & ( x . i <= r9 . i or l9 . i <= x . i ) ) by A2, A22, Th20;

hence contradiction by A20; :: thesis: verum

hereby :: thesis: verum

assume A23:
l9 . i0 > l . i0
; :: thesis: contradiction

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

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

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

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

A33: l . i0 > r . i0 by A1;

( x . i0 >= l . i0 or r . i0 >= x . i0 ) by A32;

then A34: x in cell (l,r) by A33;

( not r9 . i0 >= x . i0 or not x . i0 >= l9 . i0 ) by A3, XXREAL_0:2;

then ex i being Element of Seg d st

( l9 . i > r9 . i & ( x . i <= r9 . i or l9 . i <= x . i ) ) by A2, A34, Th20;

hence contradiction by A32; :: thesis: verum

end;defpred S

A24: 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
( ( i = i0 & r9 . i >= l . i ) or ( i = i0 & l . i >= r9 . i ) or i <> i0 )
;

end;

suppose A25:
( i = i0 & r9 . i >= l . i )
; :: thesis: ex xi being Element of REAL st S_{1}[i,xi]

l9 . i > r9 . i
by A3;

then consider xi being Element of REAL such that

A26: r9 . i < xi and

A27: xi < l9 . i by Th1;

xi > l . i by A25, A26, XXREAL_0:2;

hence ex xi being Element of REAL st S_{1}[i,xi]
by A26, A27; :: thesis: verum

end;then consider xi being Element of REAL such that

A26: r9 . i < xi and

A27: xi < l9 . i by Th1;

xi > l . i by A25, A26, XXREAL_0:2;

hence ex xi being Element of REAL st S

suppose A28:
( i = i0 & l . i >= r9 . i )
; :: thesis: ex xi being Element of REAL st S_{1}[i,xi]

then consider xi being Element of REAL such that

A29: l . i < xi and

A30: xi < l9 . i by A23, Th1;

xi > r9 . i by A28, A29, XXREAL_0:2;

hence ex xi being Element of REAL st S_{1}[i,xi]
by A29, A30; :: thesis: verum

end;A29: l . i < xi and

A30: xi < l9 . i by A23, Th1;

xi > r9 . i by A28, A29, XXREAL_0:2;

hence ex xi being Element of REAL st S

A32: for i being Element of Seg d holds S

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

A33: l . i0 > r . i0 by A1;

( x . i0 >= l . i0 or r . i0 >= x . i0 ) by A32;

then A34: x in cell (l,r) by A33;

( not r9 . i0 >= x . i0 or not x . i0 >= l9 . i0 ) by A3, XXREAL_0:2;

then ex i being Element of Seg d st

( l9 . i > r9 . i & ( x . i <= r9 . i or l9 . i <= x . i ) ) by A2, A34, Th20;

hence contradiction by A32; :: thesis: verum

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

then reconsider x = x as Element of REAL d ;

set i0 = the Element of Seg d;

A37: r . the Element of Seg d <= r9 . the Element of Seg d by A35;

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

then A38: r . the Element of Seg d < l9 . the Element of Seg d by A37, XXREAL_0:2;

l9 . the Element of Seg d <= l . the Element of Seg d by A35;

then r . the Element of Seg d < l . the Element of Seg d by A38, XXREAL_0:2;

then ( x . the Element of Seg d < l . the Element of Seg d or r . the Element of Seg d < x . the Element of Seg d ) by XXREAL_0:2;

then consider i being Element of Seg d such that

r . i < l . i and

A39: ( x . i <= r . i or l . i <= x . i ) by A36, Th20;

A40: r . i <= r9 . i by A35;

A41: l9 . i <= l . i by A35;

A42: r9 . i < l9 . i by A35;

( x . i <= r9 . i or l9 . i <= x . i ) by A39, A40, A41, XXREAL_0:2;

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