:: deftheorem Def4 defines OpenHyperInterval SRINGS_5:def 15 :
for n being Nat
for a, b being Element of REAL n
for b₄ being Subset of (REAL n) holds
( b₄ = OpenHyperInterval (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).[ ) ) ) );