let X be non empty almost_discrete TopSpace; :: thesis: for A being Subset of X st A is maximal_discrete holds
union { (Cl {a}) where a is Point of X : a in A } = the carrier of X
let A be Subset of X; :: thesis: ( A is maximal_discrete implies union { (Cl {a}) where a is Point of X : a in A } = the carrier of X )
assume A is maximal_discrete ; :: thesis: union { (Cl {a}) where a is Point of X : a in A } = the carrier of X
then A is dense by Th56;
then Cl A = the carrier of X by TOPS_3:def 2;
hence union { (Cl {a}) where a is Point of X : a in A } = the carrier of X by Th48; :: thesis: verum