:: deftheorem Def1 defines OpenHypercube TIETZE_2:def 1 :
for n being Nat
for p being Point of (TOP-REAL n)
for r being Real
for b₄ being open Subset of (TOP-REAL n) holds
( b₄ = OpenHypercube (p,r) iff ex e being Point of (Euclid n) st
( p = e & b₄ = OpenHypercube (e,r) ) );