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 ) ) );

set CELL = { x where x is Element of REAL d : S_{1}[x] } ;

S_{1}[l]
;

then A1: l in { x where x is Element of REAL d : S_{1}[x] }
;

{ x where x is Element of REAL d : S_{1}[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

( 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

S

then A1: l in { x where x is Element of REAL d : S

{ x where x is Element of REAL d : S

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