theorem Th23: :: COMPL_SP:23

for T being non empty TopSpace
for F being Subset-Family of T
for S being SetSequence of T st rng S c= F & S is non-empty holds
ex R being non-empty closed SetSequence of T st
( R is non-ascending & ( F is locally_finite & S is one-to-one implies meet R = {} ) & ( for i being Nat ex Si being Subset-Family of T st
( R . i = Cl (union Si) & Si = { (S . j) where j is Element of NAT : j >= i } ) ) )