:: deftheorem Def5 defines DiscrWithInfin TOPGEN_2:def 5 :
for X, x0 being set
for b₃ being strict TopStruct holds
( b₃ = DiscrWithInfin (X,x0) iff ( the carrier of b₃ = X & the topology of b₃ = { U where U is Subset of X : not x0 in U } \/ { (F `) where F is Subset of X : F is finite } ) );