for n being Nat
for b being Element of REAL n
for p being Point of (TOP-REAL n) ex a being Element of REAL n st
( a = p & ClosedHypercube (p,b) = ClosedHyperInterval ((a - b),(a + b)) )