theorem Th21: :: EUCLID_9:21

for n being Nat
for r being Real
for e, e1 being Point of (Euclid n) holds OpenHypercube (e1,(r - ((abs (e1 - e)) . (max_diff_index (e1,e))))) c= OpenHypercube (e,r)