let d be non zero Element of NAT ; :: thesis: for l', r', l, r being Element of REAL d st ( for i being Element of Seg d holds l' . i <= r' . i ) holds
( cell l,r c= cell l',r' iff for i being Element of Seg d holds
( l' . i <= l . i & l . i <= r . i & r . i <= r' . i ) )
let l', r', l, r be Element of REAL d; :: thesis: ( ( for i being Element of Seg d holds l' . i <= r' . i ) implies ( cell l,r c= cell l',r' iff for i being Element of Seg d holds
( l' . i <= l . i & l . i <= r . i & r . i <= r' . i ) ) )
assume A1: for i being Element of Seg d holds l' . i <= r' . i ; :: thesis: ( cell l,r c= cell l',r' iff for i being Element of Seg d holds
( l' . i <= l . i & l . i <= r . i & r . i <= r' . i ) )
thus ( cell l,r c= cell l',r' implies for i being Element of Seg d holds
( l' . i <= l . i & l . i <= r . i & r . i <= r' . i ) ) :: thesis: ( ( for i being Element of Seg d holds
( l' . i <= l . i & l . i <= r . i & r . i <= r' . 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
( l' . i <= l . i & l . i <= r . i & r . i <= r' . i )
let i0 be Element of Seg d; :: thesis: ( l' . i0 <= l . i0 & l . i0 <= r . i0 & r . i0 <= r' . i0 )

per cases ( r . i0 < l . i0 or l . i0 <= r . i0 ) ;

suppose A3: r . i0 < l . i0 ; :: thesis: ( l' . i0 <= l . i0 & l . i0 <= r . i0 & r . i0 <= r' . i0 )

defpred S₁[ Element of Seg d, Real] means ( $2 > l . $1 & $2 > r' . $1 );
A4: for i being Element of Seg d ex xi being Real st S₁[i,xi] by Th2;
consider x being Function of Seg d, REAL such that
A5: for i being Element of Seg d holds S₁[i,x . i] from FUNCT_2:sch 3(A4);
reconsider x = x as Element of REAL d by Def4;
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 A3, A5; :: thesis: verum

end;

then A6: x in cell l,r ;
ex i being Element of Seg d st
( x . i < l' . i or r' . i < x . i )

proof

take i0 ; :: thesis: ( x . i0 < l' . i0 or r' . i0 < x . i0 )
thus ( x . i0 < l' . i0 or r' . i0 < x . i0 ) by A5; :: thesis: verum

end;

hence ( l' . i0 <= l . i0 & l . i0 <= r . i0 & r . i0 <= r' . i0 ) by A1, A2, A6, Th25; :: thesis: verum

end;

suppose A7: l . i0 <= r . i0 ; :: thesis: ( l' . i0 <= l . i0 & l . i0 <= r . i0 & r . i0 <= r' . i0 )

A8: l in cell l,r by Th27;
r in cell l,r by Th27;
hence ( l' . i0 <= l . i0 & l . i0 <= r . i0 & r . i0 <= r' . i0 ) by A1, A2, A7, A8, Th25; :: thesis: verum

end;

end;

end;

assume A9: for i being Element of Seg d holds
( l' . i <= l . i & l . i <= r . i & r . i <= r' . 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 A10: x in cell l,r ; :: thesis: x in cell l',r'
then reconsider x = x as Element of REAL d ;

now

let i be Element of Seg d; :: thesis: ( l' . i <= x . i & x . i <= r' . i & l' . i <= r' . i )
A11: l' . i <= l . i by A9;
A12: l . i <= x . i by A9, A10, Th25;
A13: x . i <= r . i by A9, A10, Th25;
r . i <= r' . i by A9;
hence ( l' . i <= x . i & x . i <= r' . i ) by A11, A12, A13, XXREAL_0:2; :: thesis: l' . i <= r' . i
hence l' . i <= r' . i by XXREAL_0:2; :: thesis: verum

end;

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