theorem Th25: :: SRINGS_5:26

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
for x being object holds
( x in O iff ex y being object st
( y in NAT & x in s . y ) )