:: deftheorem Def2 defines ClosedHypercube TIETZE_2:def 2 :
for n being Nat
for p being Point of (TOP-REAL n)
for R being real-valued FinSequence
for b₄ being Subset of (TOP-REAL n) holds
( b₄ = ClosedHypercube (p,R) iff for q being Point of (TOP-REAL n) holds
( q in b₄ iff for i being Nat st i in Seg n holds
q . i in [.((p . i) - (R . i)),((p . i) + (R . i)).] ) );