theorem Th20: :: TOPS_2:20

for GX being TopSpace
for W being Subset-Family of GX st W is open & W is finite holds
meet W is open