theorem :: TOPGEN_2:23

for X, x0 being set st X is infinite holds
for U being Subset of (DiscrWithInfin (X,x0)) st U = {x0} holds
not U is open