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