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 ) ) );
set CELL = { x where x is Element of REAL d : S₁[x] } ;
S₁[l] ;
then A1: l in { x where x is Element of REAL d : S₁[x] } ;
{ x where x is Element of REAL d : S₁[x] } c= REAL d from FRAENKEL:sch 10();
hence { x where x is Element of REAL d : ( 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 ) ) ) } is non empty Subset of (REAL d) by A1; :: thesis: verum