theorem Th4: :: COMPACT1:4

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