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