for n being Nat
for V being Subset of (TopSpaceMetr (Euclid n)) st V is open holds
for e being Point of (Euclid n) st e in V holds
ex m being non zero Element of NAT st OpenHypercube (e,(1 / m)) c= V