theorem :: TEX_1:23

for D being non empty set
for d0 being Element of D st not D \ {d0} is empty holds
for A being Subset of (STS (D,d0)) holds
( ( A = D \ {d0} implies ( A is open & A is dense ) ) & ( A <> D & A is open & A is dense implies A = D \ {d0} ) )