:: deftheorem defines Up CONNSP_3:def 4 :
for GX being TopStruct
for B being Subset of GX
for p being Point of (GX | B) st B <> {} holds
Up p = p;