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 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 ;
suppose for i being Element of Seg d holds
( l9 . i <= x . i & x . i <= r9 . i ) ; :: thesis: contradiction
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
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 ;
hence ex xi being Element of REAL st S1[i,xi] by ; :: 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 ;
xi < l9 . i by ;
hence ex xi being Element of REAL st S1[i,xi] by ; :: 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 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 ;
then ex i being Element of Seg d st
( r9 . i < l9 . i & ( x . i <= r9 . i or l9 . i <= x . i ) ) by ;
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 ;
hence ex xi being Element of REAL st S1[i,xi] by ; :: 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 ;
xi > r9 . i by ;
hence ex xi being Element of REAL st S1[i,xi] by ; :: 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 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 ;
then ex i being Element of Seg d st
( l9 . i > r9 . i & ( x . i <= r9 . i or l9 . i <= x . i ) ) by ;
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 ;
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 ;
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 ;
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 ;
hence x in cell (l9,r9) by A42; :: thesis: verum