theorem :: EUCLID_9:18

for n being Nat
for r being Real
for e being Point of (Euclid n) st n <> 0 holds
OpenHypercube (e,r) c= Ball (e,(r * (sqrt n)))