:: deftheorem Def5 defines LeftOpenHyperInterval SRINGS_5:def 16 :
for n being Nat
for a, b being Element of REAL n
for b₄ being Subset of (REAL n) holds
( b₄ = LeftOpenHyperInterval (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).] ) ) ) );