let d be non zero Element of NAT ; :: thesis: for x, l, r 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 x, l, r 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₁[ 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 = { x' where x' is Element of REAL d : S₁[x'] } ;
thus ( x in cell l,r iff S₁[x] ) from LMOD_7:sch 7(A1); :: thesis: verum