for n being Nat
for O being open Subset of (TOP-REAL n) ex Y being Subset of (dense_countable_OpenHypercubes n) st
( Y is countable & O = union Y )