theorem Th19: :: EUCLID_9:19

for n being Nat
for r being Real
for e, e1 being Point of (Euclid n) st e1 in Ball (e,r) holds
ex m being non zero Element of NAT st OpenHypercube (e1,(1 / m)) c= Ball (e,r)