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

( 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