theorem :: SRINGS_5:22

for n being Nat holds dense_countable_OpenHypercubes n = { (OpenHypercube (q,(1 / m))) where q is Point of (Euclid n), m is positive Nat : q in RAT n }