theorem Th22: :: EUCLID_9:22

for n being Nat
for r being Real
for e being Point of (Euclid n) holds Ball (e,r) c= OpenHypercube (e,r)