let n be Nat; :: thesis: for O being non empty open Subset of (TOP-REAL n) ex Y being Subset of (dense_countable_OpenHypercubes n) st
( not Y is empty & O = union Y & 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 ) ) )
let O be non empty open Subset of (TOP-REAL n); :: thesis: ex Y being Subset of (dense_countable_OpenHypercubes n) st
( not Y is empty & O = union Y & 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 ) ) )
consider Y being Subset of (dense_countable_OpenHypercubes n) such that
Y is countable and
A1: O = union Y by Th23;
take Y ; :: thesis: ( not Y is empty & O = union Y & 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 ) ) )
thus not Y is empty by A1, ZFMISC_1:2; :: thesis: ( O = union Y & 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 ) ) )
thus O = union Y by A1; :: thesis: 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 ) )
consider g being Function of omega,Y such that
A2: rng g = Y by A1, ZFMISC_1:2, CARD_3:96;
take g ; :: thesis: for x being object holds
( x in O iff ex y being object st
( y in NAT & x in g . y ) )
A3: dom g = omega by A1, ZFMISC_1:2, FUNCT_2:def 1;
O = Union g by A1, A2;
hence for x being object holds
( x in O iff ex y being object st
( y in NAT & x in g . y ) ) by A3, CARD_5:2; :: thesis: verum