for n being Nat holds dense_countable_OpenHypercubes n is countable Basis of (TOP-REAL n) by Th21;