let d be non zero Element of NAT ; :: thesis: for r, l, l', r' being Element of REAL d st ( for i being Element of Seg d holds r . i < l . i ) holds
( cell l,r c= cell l',r' iff for i being Element of Seg d holds
( r . i <= r' . i & r' . i < l' . i & l' . i <= l . i ) )
let r, l, l', r' be Element of REAL d; :: thesis: ( ( for i being Element of Seg d holds r . i < l . i ) implies ( cell l,r c= cell l',r' iff for i being Element of Seg d holds
( r . i <= r' . i & r' . i < l' . i & l' . i <= l . i ) ) )
assume A1: for i being Element of Seg d holds r . i < l . i ; :: thesis: ( cell l,r c= cell l',r' iff for i being Element of Seg d holds
( r . i <= r' . i & r' . i < l' . i & l' . i <= l . i ) )
thus ( cell l,r c= cell l',r' implies for i being Element of Seg d holds
( r . i <= r' . i & r' . i < l' . i & l' . i <= l . i ) ) :: thesis: ( ( for i being Element of Seg d holds
( r . i <= r' . i & r' . i < l' . i & l' . i <= l . i ) ) implies cell l,r c= cell l',r' )
proof
assume A2: cell l,r c= cell l',r' ; :: thesis: for i being Element of Seg d holds
( r . i <= r' . i & r' . i < l' . i & l' . i <= l . i )
A3: for i being Element of Seg d holds r' . i < l' . i
proof
let i0 be Element of Seg d; :: thesis: r' . i0 < l' . i0
assume A4: l' . i0 <= r' . i0 ; :: thesis: contradiction
defpred S1[ Element of Seg d, Real] means ( ( $1 = i0 implies ( l . $1 < $2 & r' . $1 < $2 ) ) & ( r' . $1 < l' . $1 implies ( r' . $1 < $2 & $2 < l' . $1 ) ) );
A5: for i being Element of Seg d ex xi being Real st S1[i,xi]
proof
let i be Element of Seg d; :: thesis: ex xi being Real st S1[i,xi]
per cases ( ( i = i0 & r' . i < l' . i ) or i <> i0 or l' . i <= r' . i ) ;
suppose ( i = i0 & r' . i < l' . i ) ; :: thesis: ex xi being Real st S1[i,xi]
hence ex xi being Real st S1[i,xi] by A4; :: thesis: verum
end;
suppose A6: i <> i0 ; :: thesis: ex xi being Real st S1[i,xi]
( r' . i < l' . i implies ex xi being Real st
( r' . i < xi & xi < l' . i ) ) by Th1;
hence ex xi being Real st S1[i,xi] by A6; :: thesis: verum
end;
suppose A7: l' . i <= r' . i ; :: thesis: ex xi being Real st S1[i,xi]
ex xi being Real st
( l . i < xi & r' . i < xi ) by Th2;
hence ex xi being 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 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
( l' . i <= x . i & x . i <= r' . i ) or ex i being Element of Seg d st
( r' . i < l' . i & ( x . i <= r' . i or l' . i <= x . i ) ) ) by A2, A10, Th24;
suppose for i being Element of Seg d holds
( l' . i <= x . i & x . i <= r' . i ) ; :: thesis: contradiction
then x . i0 <= r' . i0 ;
hence contradiction by A8; :: thesis: verum
end;
suppose ex i being Element of Seg d st
( r' . i < l' . i & ( x . i <= r' . i or l' . i <= x . i ) ) ; :: thesis: contradiction
hence contradiction by A8; :: thesis: verum
end;
end;
end;
let i0 be Element of Seg d; :: thesis: ( r . i0 <= r' . i0 & r' . i0 < l' . i0 & l' . i0 <= l . i0 )
hereby :: thesis: ( r' . i0 < l' . i0 & l' . i0 <= l . i0 )
assume A11: r' . i0 < r . i0 ; :: thesis: contradiction
defpred S1[ Element of Seg d, Real] means ( r' . $1 < $2 & $2 < l' . $1 & ( $1 = i0 implies $2 < r . $1 ) );
A12: for i being Element of Seg d ex xi being Real st S1[i,xi]
proof
let i be Element of Seg d; :: thesis: ex xi being Real st S1[i,xi]
per cases ( ( i = i0 & l' . i <= r . i ) or ( i = i0 & r . i <= l' . i ) or i <> i0 ) ;
suppose A13: ( i = i0 & l' . i <= r . i ) ; :: thesis: ex xi being Real st S1[i,xi]
r' . i < l' . i by A3;
then consider xi being Real such that
A14: r' . i < xi and
A15: xi < l' . i by Th1;
xi < r . i by A13, A15, XXREAL_0:2;
hence ex xi being Real st S1[i,xi] by A14, A15; :: thesis: verum
end;
suppose A16: ( i = i0 & r . i <= l' . i ) ; :: thesis: ex xi being Real st S1[i,xi]
then consider xi being Real such that
A17: r' . i < xi and
A18: xi < r . i by A11, Th1;
xi < l' . i by A16, A18, XXREAL_0:2;
hence ex xi being Real st S1[i,xi] by A17, A18; :: thesis: verum
end;
suppose A19: i <> i0 ; :: thesis: ex xi being Real st S1[i,xi]
r' . i < l' . i by A3;
then ex xi being Real st
( r' . i < xi & xi < l' . i ) by Th1;
hence ex xi being 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 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 l' . i0 <= x . i0 or not x . i0 <= r' . i0 ) by A3, XXREAL_0:2;
then ex i being Element of Seg d st
( r' . i < l' . i & ( x . i <= r' . i or l' . i <= x . i ) ) by A2, A22, Th24;
hence contradiction by A20; :: thesis: verum
end;
thus r' . i0 < l' . i0 by A3; :: thesis: l' . i0 <= l . i0
hereby :: thesis: verum
assume A23: l' . i0 > l . i0 ; :: thesis: contradiction
defpred S1[ Element of Seg d, Real] means ( l' . $1 > $2 & $2 > r' . $1 & ( $1 = i0 implies $2 > l . $1 ) );
A24: for i being Element of Seg d ex xi being Real st S1[i,xi]
proof
let i be Element of Seg d; :: thesis: ex xi being Real st S1[i,xi]
per cases ( ( i = i0 & r' . i >= l . i ) or ( i = i0 & l . i >= r' . i ) or i <> i0 ) ;
suppose A25: ( i = i0 & r' . i >= l . i ) ; :: thesis: ex xi being Real st S1[i,xi]
l' . i > r' . i by A3;
then consider xi being Real such that
A26: r' . i < xi and
A27: xi < l' . i by Th1;
xi > l . i by A25, A26, XXREAL_0:2;
hence ex xi being Real st S1[i,xi] by A26, A27; :: thesis: verum
end;
suppose A28: ( i = i0 & l . i >= r' . i ) ; :: thesis: ex xi being Real st S1[i,xi]
then consider xi being Real such that
A29: l . i < xi and
A30: xi < l' . i by A23, Th1;
xi > r' . i by A28, A29, XXREAL_0:2;
hence ex xi being Real st S1[i,xi] by A29, A30; :: thesis: verum
end;
suppose A31: i <> i0 ; :: thesis: ex xi being Real st S1[i,xi]
l' . i > r' . i by A3;
then ex xi being Real st
( r' . i < xi & xi < l' . i ) by Th1;
hence ex xi being 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 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 r' . i0 >= x . i0 or not x . i0 >= l' . i0 ) by A3, XXREAL_0:2;
then ex i being Element of Seg d st
( l' . i > r' . i & ( x . i <= r' . i or l' . 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 <= r' . i & r' . i < l' . i & l' . i <= l . i ) ; :: thesis: cell l,r c= cell l',r'
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in cell l,r or x in cell l',r' )
assume A36: x in cell l,r ; :: thesis: x in cell l',r'
then reconsider x = x as Element of REAL d ;
consider i0 being Element of Seg d;
A37: r . i0 <= r' . i0 by A35;
r' . i0 < l' . i0 by A35;
then A38: r . i0 < l' . i0 by A37, XXREAL_0:2;
l' . i0 <= l . i0 by A35;
then r . i0 < l . i0 by A38, XXREAL_0:2;
then ( x . i0 < l . i0 or r . i0 < x . i0 ) 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 <= r' . i by A35;
A41: l' . i <= l . i by A35;
A42: r' . i < l' . i by A35;
( x . i <= r' . i or l' . i <= x . i ) by A39, A40, A41, XXREAL_0:2;
hence x in cell l',r' by A42; :: thesis: verum