theorem :: SRINGS_5:23

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