theorem :: SRINGS_5:106

for r being Real
for n being non zero Nat
for p being Element of (EMINFTY n)
for e being Point of (Euclid n) st e = p holds
Ball (p,r) = OpenHypercube (e,r)