:: deftheorem Def9 defines One-Point_Compactification COMPACT1:def 9 :
for X being TopStruct
for b₂ being strict TopStruct holds
( b₂ = One-Point_Compactification X iff ( the carrier of b₂ = succ ([#] X) & the topology of b₂ = the topology of X \/ { (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact ) } ) );