theorem Th51: :: SRINGS_5:75

for r being Real
for n being non zero Nat
for e being Point of (Euclid n) ex a being Element of REAL n st
( a = e & OpenHypercube (e,r) = OpenHyperInterval ((a - (n |-> r)),(a + (n |-> r))) )