theorem :: TEX_2:27

for Y being TopStruct
for A being Subset of Y st A is discrete holds
for x being Point of Y st x in A holds
ex F being Subset of Y st
( F is closed & A /\ F = {x} )