theorem Th24: :: SRINGS_5:25

for n being Nat
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 ) ) )