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) )
proof
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
proof
let i0 be Element of Seg d; :: thesis: r9 . i0 < l9 . i0
assume A4: l9 . i0 <= r9 . i0 ; :: thesis: contradiction
defpred S1[ 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 S1[i,xi]
proof
let i be Element of Seg d; :: thesis: ex xi being Element of REAL st S1[i,xi]
per cases ( ( i = i0 & r9 . i < l9 . i ) or i <> i0 or l9 . i <= r9 . i ) ;
suppose ( i = i0 & r9 . i < l9 . i ) ; :: thesis: ex xi being Element of REAL st S1[i,xi]
hence ex xi being Element of REAL st S1[i,xi] by A4; :: thesis: verum
end;
suppose A6: i <> i0 ; :: thesis: ex xi being Element of REAL st S1[i,xi]
( r9 . i < l9 . i implies ex xi being Element of REAL st
( r9 . i < xi & xi < l9 . i ) ) by Th1;
hence ex xi being Element of REAL st S1[i,xi] by A6; :: thesis: verum
end;
suppose A7: l9 . i <= r9 . i ; :: thesis: ex xi being Element of REAL st S1[i,xi]
ex xi being Element of REAL st
( l . i < xi & r9 . i < xi ) by Th2;
hence ex xi being Element of REAL st S1[i,xi] by A7; :: thesis: verum
end;
end;
end;
consider x being Function of (Seg d),REAL such that
A8: for i being Element of Seg d holds S1[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;
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;
suppose for i being Element of Seg d holds
( l9 . i <= x . i & x . i <= r9 . i ) ; :: thesis: contradiction
then x . i0 <= r9 . i0 ;
hence contradiction by A8; :: thesis: verum
end;
suppose ex i being Element of Seg d st
( r9 . i < l9 . i & ( x . i <= r9 . i or l9 . i <= x . i ) ) ; :: thesis: contradiction
hence contradiction by A8; :: thesis: verum
end;
end;
end;
let i0 be Element of Seg d; :: thesis: ( r . i0 <= r9 . i0 & r9 . i0 < l9 . i0 & l9 . i0 <= l . i0 )
hereby :: thesis: ( r9 . i0 < l9 . i0 & l9 . i0 <= l . i0 )
assume A11: r9 . i0 < r . i0 ; :: thesis: contradiction
defpred S1[ 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 S1[i,xi]
proof
let i be Element of Seg d; :: thesis: ex xi being Element of REAL st S1[i,xi]
per cases ( ( i = i0 & l9 . i <= r . i ) or ( i = i0 & r . i <= l9 . i ) or i <> i0 ) ;
suppose A13: ( i = i0 & l9 . i <= r . i ) ; :: thesis: ex xi being Element of REAL st S1[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 S1[i,xi] by A14, A15; :: thesis: verum
end;
suppose A16: ( i = i0 & r . i <= l9 . i ) ; :: thesis: ex xi being Element of REAL st S1[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 S1[i,xi] by A17, A18; :: thesis: verum
end;
suppose A19: i <> i0 ; :: thesis: ex xi being Element of REAL st S1[i,xi]
r9 . i < l9 . i by A3;
then ex xi being Element of REAL st
( r9 . i < xi & xi < l9 . i ) by Th1;
hence ex xi being Element of REAL st S1[i,xi] by A19; :: thesis: verum
end;
end;
end;
consider x being Function of (Seg d),REAL such that
A20: for i being Element of Seg d holds S1[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;
thus r9 . i0 < l9 . i0 by A3; :: thesis: l9 . i0 <= l . i0
hereby :: thesis: verum
assume A23: l9 . i0 > l . i0 ; :: thesis: contradiction
defpred S1[ 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 S1[i,xi]
proof
let i be Element of Seg d; :: thesis: ex xi being Element of REAL st S1[i,xi]
per cases ( ( i = i0 & r9 . i >= l . i ) or ( i = i0 & l . i >= r9 . i ) or i <> i0 ) ;
suppose A25: ( i = i0 & r9 . i >= l . i ) ; :: thesis: ex xi being Element of REAL st S1[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 S1[i,xi] by A26, A27; :: thesis: verum
end;
suppose A28: ( i = i0 & l . i >= r9 . i ) ; :: thesis: ex xi being Element of REAL st S1[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 S1[i,xi] by A29, A30; :: thesis: verum
end;
suppose A31: i <> i0 ; :: thesis: ex xi being Element of REAL st S1[i,xi]
l9 . i > r9 . i by A3;
then ex xi being Element of REAL st
( r9 . i < xi & xi < l9 . i ) by Th1;
hence ex xi being Element of REAL st S1[i,xi] by A31; :: thesis: verum
end;
end;
end;
consider x being Function of (Seg d),REAL such that
A32: for i being Element of Seg d holds S1[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;
end;
assume A35: for i being Element of Seg d holds
( 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