for n being Nat
for p being Point of (TOP-REAL n)
for r being Real
for R being real-valued FinSequence st n <= len R & r <= inf (rng R) holds
OpenHypercube (p,r) c= ClosedHypercube (p,R)