:: deftheorem Def6 defines RightOpenHyperInterval SRINGS_5:def 17 :
for n being Nat
for a, b being Element of REAL n
for b₄ being Subset of (REAL n) holds
( b₄ = RightOpenHyperInterval (a,b) iff for x being object holds
( x in b₄ iff ex y being Element of REAL n st
( x = y & ( for i being Nat st i in Seg n holds
y . i in [.(a . i),(b . i).[ ) ) ) );