theorem :: TEX_1:15

for X being non empty TopSpace st ( for A being Subset of X st A <> the carrier of X holds
A is boundary ) holds
X is anti-discrete