for X being non empty almost_discrete TopSpace ex M being Subset of X st M is maximal_discrete