for n being Nat
for O being non empty open Subset of (TOP-REAL n) ex s being sequence of (dense_countable_OpenHypercubes n) st O = Union s