theorem Th20: :: EUCLID_9:20

for n being Nat
for r being Real
for e, e1 being Point of (Euclid n) st n <> 0 & e1 in OpenHypercube (e,r) holds
r > (abs (e1 - e)) . (max_diff_index (e1,e))