let X be non empty almost_discrete TopSpace; :: thesis: ex M being Subset of X st M is maximal_discrete
set A = {} X;
{} X is discrete by Th29;
then consider M being Subset of X such that
{} X c= M and
A1: M is maximal_discrete by Th59;
take M ; :: thesis: M is maximal_discrete
thus M is maximal_discrete by A1; :: thesis: verum