let d be non zero Nat; :: thesis: for l, r, x being Element of REAL d holds

( x in cell (l,r) iff ( for i being Element of Seg d holds

( l . i <= x . i & x . i <= r . i ) or 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: ( x in cell (l,r) iff ( for i being Element of Seg d holds

( l . i <= x . i & x . i <= r . i ) or ex i being Element of Seg d st

( r . i < l . i & ( x . i <= r . i or l . i <= x . i ) ) ) )

defpred S_{1}[ Element of REAL d] means ( for i being Element of Seg d holds

( l . i <= $1 . i & $1 . i <= r . i ) or ex i being Element of Seg d st

( r . i < l . i & ( $1 . i <= r . i or l . i <= $1 . i ) ) );

A1: cell (l,r) = { x9 where x9 is Element of REAL d : S_{1}[x9] }
;

thus ( x in cell (l,r) iff S_{1}[x] )
from LMOD_7:sch 7(A1); :: thesis: verum

( x in cell (l,r) iff ( for i being Element of Seg d holds

( l . i <= x . i & x . i <= r . i ) or 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: ( x in cell (l,r) iff ( for i being Element of Seg d holds

( l . i <= x . i & x . i <= r . i ) or ex i being Element of Seg d st

( r . i < l . i & ( x . i <= r . i or l . i <= x . i ) ) ) )

defpred S

( l . i <= $1 . i & $1 . i <= r . i ) or ex i being Element of Seg d st

( r . i < l . i & ( $1 . i <= r . i or l . i <= $1 . i ) ) );

A1: cell (l,r) = { x9 where x9 is Element of REAL d : S

thus ( x in cell (l,r) iff S