theorem Th13: :: COMPL_SP:13

for T being non empty TopSpace
for F being Subset-Family of T
for S being SetSequence of T st rng S c= F holds
ex R being SetSequence of T st
( R is non-ascending & ( F is centered implies R is non-empty ) & ( F is open implies R is open ) & ( F is closed implies R is closed ) & ( for i being Nat holds R . i = meet { (S . j) where j is Element of NAT : j <= i } ) )