:: deftheorem Def6 defines CofinTop YELLOW_8:def 6 :
for X being set
for b₂ being strict TopStruct holds
( b₂ = CofinTop X iff ( the carrier of b₂ = X & COMPLEMENT the topology of b₂ = {X} \/ (Fin X) ) );