let d be non zero Nat; :: thesis: for l, r, x being Element of REAL d st ex i being Element of Seg d st r . i < l . i holds
( x in cell (l,r) iff ex i being Element of Seg d st
( r . i < l . i & ( x . i <= r . i or l . i <= x . i ) ) )
let l, r, x be Element of REAL d; :: thesis: ( ex i being Element of Seg d st r . i < l . i implies ( x in cell (l,r) iff ex i being Element of Seg d st
( r . i < l . i & ( x . i <= r . i or l . i <= x . i ) ) ) )
given i0 being Element of Seg d such that A1: r . i0 < l . i0 ; :: thesis: ( x in cell (l,r) iff ex i being Element of Seg d st
( r . i < l . i & ( x . i <= r . i or l . i <= x . i ) ) )
( x . i0 < l . i0 or r . i0 < x . i0 ) by A1, XXREAL_0:2;
hence ( x in cell (l,r) implies ex i being Element of Seg d st
( r . i < l . i & ( x . i <= r . i or l . i <= x . i ) ) ) by Th20; :: thesis: ( ex i being Element of Seg d st
( r . i < l . i & ( x . i <= r . i or l . i <= x . i ) ) implies x in cell (l,r) )
thus ( ex i being Element of Seg d st
( r . i < l . i & ( x . i <= r . i or l . i <= x . i ) ) implies x in cell (l,r) ) ; :: thesis: verum