for X being non empty discrete TopSpace
for A being Subset of X holds
( A is maximal_discrete iff not A is proper )