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₁[ 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₁[x9] } ;
thus ( x in cell (l,r) iff S₁[x] ) from LMOD_7:sch 7(A1); :: thesis: verum