theorem Th17: :: EUCLID_9:17

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