theorem Th17: :: NAGATA_1:17

for T being non empty TopSpace
for U being sequence of (bool the carrier of T) st ( for n being Element of NAT holds U . n is open ) holds
Union U is open