let d be non zero Nat; 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; ( 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
; ( 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; ( 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) )
; verum