let d be non zero Element of NAT ; :: thesis: for l, r, r', l' being Element of REAL d st ( for i being Element of Seg d holds l . i <= r . i ) & ( for i being Element of Seg d holds r' . i < l' . i ) holds
( cell l,r c= cell l',r' iff ex i being Element of Seg d st
( r . i <= r' . i or l' . i <= l . i ) )
let l, r, r', l' be Element of REAL d; :: thesis: ( ( for i being Element of Seg d holds l . i <= r . i ) & ( for i being Element of Seg d holds r' . i < l' . i ) implies ( cell l,r c= cell l',r' iff ex i being Element of Seg d st
( r . i <= r' . i or l' . i <= l . i ) ) )
assume A1: for i being Element of Seg d holds l . i <= r . i ; :: thesis: ( ex i being Element of Seg d st not r' . i < l' . i or ( cell l,r c= cell l',r' iff ex i being Element of Seg d st
( r . i <= r' . i or l' . i <= l . i ) ) )
assume A2: for i being Element of Seg d holds r' . i < l' . i ; :: thesis: ( cell l,r c= cell l',r' iff ex i being Element of Seg d st
( r . i <= r' . i or l' . i <= l . i ) )
thus ( cell l,r c= cell l',r' implies ex i being Element of Seg d st
( r . i <= r' . i or l' . i <= l . i ) ) :: thesis: ( ex i being Element of Seg d st
( r . i <= r' . i or l' . i <= l . i ) implies cell l,r c= cell l',r' )

proof

assume A3: cell l,r c= cell l',r' ; :: thesis: ex i being Element of Seg d st
( r . i <= r' . i or l' . i <= l . i )
assume A4: for i being Element of Seg d holds
( r' . i < r . i & l . i < l' . i ) ; :: thesis: contradiction
defpred S₁[ Element of Seg d, Real] means ( l . $1 <= $2 & $2 <= r . $1 & r' . $1 < $2 & $2 < l' . $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 ( ( l . i <= r' . i & l' . i <= r . i ) or ( r' . i < l . i & l' . i <= r . i ) or r . i < l' . i ) ;

suppose A6: ( l . i <= r' . i & l' . i <= r . i ) ; :: thesis: ex xi being Real st S₁[i,xi]

r' . i < l' . i by A2;
then consider xi being Real such that
A7: ( r' . i < xi & xi < l' . i ) by Th1;
take xi ; :: thesis: S₁[i,xi]
thus S₁[i,xi] by A6, A7, XXREAL_0:2; :: thesis: verum

end;

suppose A8: ( r' . i < l . i & l' . i <= r . i ) ; :: thesis: ex xi being Real st S₁[i,xi]

take l . i ; :: thesis: S₁[i,l . i]
thus S₁[i,l . i] by A1, A4, A8; :: thesis: verum

end;

suppose A9: r . i < l' . i ; :: thesis: ex xi being Real st S₁[i,xi]

take r . i ; :: thesis: S₁[i,r . i]
thus S₁[i,r . i] by A1, A4, A9; :: thesis: verum

end;

end;

end;

consider x being Function of (Seg d),REAL such that
A10: 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;
A11: x in cell l,r by A10;
consider i0 being Element of Seg d;
r' . i0 < l' . i0 by A2;
then ex i being Element of Seg d st
( r' . i < l' . i & ( x . i <= r' . i or l' . i <= x . i ) ) by A3, A11, Th26;
hence contradiction by A10; :: thesis: verum

end;

given i0 being Element of Seg d such that A12: ( r . i0 <= r' . i0 or l' . i0 <= l . i0 ) ; :: 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 A13: x in cell l,r ; :: thesis: x in cell l',r'
then reconsider x = x as Element of REAL d ;
A14: ( l . i0 <= x . i0 & x . i0 <= r . i0 ) by A1, A13, Th25;
ex i being Element of Seg d st
( r' . i < l' . i & ( x . i <= r' . i or l' . i <= x . i ) )

proof

take i0 ; :: thesis: ( r' . i0 < l' . i0 & ( x . i0 <= r' . i0 or l' . i0 <= x . i0 ) )
thus ( r' . i0 < l' . i0 & ( x . i0 <= r' . i0 or l' . i0 <= x . i0 ) ) by A2, A12, A14, XXREAL_0:2; :: thesis: verum

end;

hence x in cell l',r' ; :: thesis: verum