theorem Th2: :: ASCOLI:2

for S being TopSpace
for F being FinSequence of bool the carrier of S st ( for i being Nat st i in Seg (len F) holds
F /. i is compact ) holds
union (rng F) is compact