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