theorem Th15: :: EUCLID_9:15

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
Sum (sqr (e1 - e)) < n * (r ^2)