for X being non empty anti-discrete TopSpace
for A being non empty Subset of X holds
( A is discrete iff A is trivial )