for X being TopStruct holds [#] X c= [#] (One-Point_Compactification X)