theorem Th11: :: EUCLID_9:11

for n being Nat
for r being Real
for e being Point of (Euclid n) st 0 < r holds
e in OpenHypercube (e,r)