:: deftheorem defines OpenHypercubes EUCLID_9:def 5 :
for n being Nat
for e being Point of (Euclid n) holds OpenHypercubes e = { (OpenHypercube (e,(1 / m))) where m is non zero Element of NAT : verum } ;