let d be non zero Element of NAT ; :: thesis: for r, l, 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 r, l, 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 S₁[ Element of Seg d, 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 Real st S₁[i,xi]

proof

let i be Element of Seg d; :: thesis: ex xi being Real st S₁[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 Real st S₁[i,xi]

hence ex xi being Real st S₁[i,xi] by A4; :: thesis: verum

end;

suppose A6: i <> i0 ; :: thesis: ex xi being Real st S₁[i,xi]

( r9 . i < l9 . i implies ex xi being Real st
( r9 . i < xi & xi < l9 . i ) ) by Th1;
hence ex xi being Real st S₁[i,xi] by A6; :: thesis: verum

end;

suppose A7: l9 . i <= r9 . i ; :: thesis: ex xi being Real st S₁[i,xi]

ex xi being Real st
( l . i < xi & r9 . i < xi ) by Th2;
hence ex xi being Real st S₁[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 S₁[i,x . i] from FUNCT_2:sch 3(A5);
reconsider x = x as Element of REAL d by Def4;
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, Th24;

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 S₁[ Element of Seg d, 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 Real st S₁[i,xi]

proof

let i be Element of Seg d; :: thesis: ex xi being Real st S₁[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 Real st S₁[i,xi]

r9 . i < l9 . i by A3;
then consider xi being 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 Real st S₁[i,xi] by A14, A15; :: thesis: verum

end;

suppose A16: ( i = i0 & r . i <= l9 . i ) ; :: thesis: ex xi being Real st S₁[i,xi]

then consider xi being 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 Real st S₁[i,xi] by A17, A18; :: thesis: verum

end;

suppose A19: i <> i0 ; :: thesis: ex xi being Real st S₁[i,xi]

r9 . i < l9 . i by A3;
then ex xi being Real st
( r9 . i < xi & xi < l9 . i ) by Th1;
hence ex xi being Real st S₁[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 S₁[i,x . i] from FUNCT_2:sch 3(A12);
reconsider x = x as Element of REAL d by Def4;
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, Th24;
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 S₁[ Element of Seg d, 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 Real st S₁[i,xi]

proof

let i be Element of Seg d; :: thesis: ex xi being Real st S₁[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 Real st S₁[i,xi]

l9 . i > r9 . i by A3;
then consider xi being 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 Real st S₁[i,xi] by A26, A27; :: thesis: verum

end;

suppose A28: ( i = i0 & l . i >= r9 . i ) ; :: thesis: ex xi being Real st S₁[i,xi]

then consider xi being 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 Real st S₁[i,xi] by A29, A30; :: thesis: verum

end;

suppose A31: i <> i0 ; :: thesis: ex xi being Real st S₁[i,xi]

l9 . i > r9 . i by A3;
then ex xi being Real st
( r9 . i < xi & xi < l9 . i ) by Th1;
hence ex xi being Real st S₁[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 S₁[i,x . i] from FUNCT_2:sch 3(A24);
reconsider x = x as Element of REAL d by Def4;
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, Th24;
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 set ; :: 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, Th24;
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