let d be non zero Element of NAT ; :: thesis: for r, l, 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 r, l, 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 Th24; :: 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