theorem :: SRINGS_5:13

for n being Nat
for p being Point of (TOP-REAL n)
for e being Point of (Euclid n) st e = p holds
{ (OpenHypercube (e,(1 / m))) where m is non zero Element of NAT : verum } = { (OpenHypercube (p,(1 / m))) where m is non zero Element of NAT : verum }