let n be Nat; :: thesis: for O being non empty open Subset of (TOP-REAL n) ex s being sequence of (dense_countable_OpenHypercubes n) st
for x being object holds
( x in O iff ex y being object st
( y in NAT & x in s . y ) )
let O be non empty open Subset of (TOP-REAL n); :: thesis: ex s being sequence of (dense_countable_OpenHypercubes n) st
for x being object holds
( x in O iff ex y being object st
( y in NAT & x in s . y ) )
consider Y being Subset of (dense_countable_OpenHypercubes n) such that
not Y is empty and
A1: O = union Y and
A2: ex g being Function of NAT,Y st
for x being object holds
( x in O iff ex y being object st
( y in NAT & x in g . y ) ) by Th24;
consider g being Function of NAT,Y such that
A3: for x being object holds
( x in O iff ex y being object st
( y in NAT & x in g . y ) ) by A2;
reconsider g2 = g as sequence of (dense_countable_OpenHypercubes n) by A1, ZFMISC_1:2, FUNCT_2:7;
for x being object holds
( x in O iff ex y being object st
( y in NAT & x in g2 . y ) ) by A3;
hence ex s being sequence of (dense_countable_OpenHypercubes n) st
for x being object holds
( x in O iff ex y being object st
( y in NAT & x in s . y ) ) ; :: thesis: verum