theorem Th70: :: SRINGS_5:108
for r being Real
for n being non zero Nat
for p being Point of (TOP-REAL n)
for q being Element of (EMINFTY n) st q = p holds
cl_Ball (q,r) = ClosedHypercube (p,(n |-> r))