:: deftheorem defines Down CONNSP_3:def 5 :
for GX being TopStruct
for V, B being Subset of GX holds Down (V,B) = V /\ B;