:: deftheorem defines Up CONNSP_3:def 6 :
for GX being TopStruct
for B being Subset of GX
for V being Subset of (GX | B) holds Up V = V;