let n be Nat; :: thesis: 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 )
let O be open Subset of (TOP-REAL n); :: thesis: ex Y being Subset of (dense_countable_OpenHypercubes n) st
( Y is countable & O = union Y )
the topology of (TOP-REAL n) c= UniCl (dense_countable_OpenHypercubes n) by Th21, CANTOR_1:def 2;
then O in UniCl (dense_countable_OpenHypercubes n) by PRE_TOPC:def 2;
then consider Y being Subset-Family of (TOP-REAL n) such that
A1: Y c= dense_countable_OpenHypercubes n and
A2: O = union Y by CANTOR_1:def 1;
thus ex Y being Subset of (dense_countable_OpenHypercubes n) st
( Y is countable & O = union Y ) by A1, A2; :: thesis: verum