theorem :: TOPGEN_2:28

for X, x0 being set st x0 in X holds
for A being Subset of (DiscrWithInfin (X,x0)) st A ` is infinite holds
Int A = A \ {x0}