for GX being TopSpace
for V, B being Subset of GX st V is open holds
Down (V,B) is open