let X be non empty almost_discrete TopSpace; :: thesis: for A being Subset of X holds Cl A = union { (Cl {a}) where a is Point of X : a in A }
let A be Subset of X; :: thesis: Cl A = union { (Cl {a}) where a is Point of X : a in A }
set F = { (Cl {a}) where a is Point of X : a in A } ;

now

let C be set ; :: thesis: ( C in { (Cl {a}) where a is Point of X : a in A } implies C in bool the carrier of X )
assume C in { (Cl {a}) where a is Point of X : a in A } ; :: thesis: C in bool the carrier of X
then ex a being Point of X st
( C = Cl {a} & a in A ) ;
hence C in bool the carrier of X ; :: thesis: verum

end;

then reconsider F = { (Cl {a}) where a is Point of X : a in A } as Subset-Family of X by TARSKI:def 3;
reconsider F = F as Subset-Family of X ;

now

let x be set ; :: thesis: ( x in A implies x in union F )
assume A1: x in A ; :: thesis: x in union F
then reconsider a = x as Point of X ;
Cl {a} in F by A1;
then A2: Cl {a} c= union F by ZFMISC_1:92;
A3: {a} c= Cl {a} by PRE_TOPC:48;
a in {a} by TARSKI:def 1;
then a in Cl {a} by A3;
hence x in union F by A2; :: thesis: verum

end;

then A4: A c= union F by TARSKI:def 3;

now

let C be set ; :: thesis: ( C in F implies C c= Cl A )
assume C in F ; :: thesis: C c= Cl A
then consider a being Point of X such that
A5: C = Cl {a} and
A6: a in A ;
{a} c= A by A6, ZFMISC_1:37;
hence C c= Cl A by A5, PRE_TOPC:49; :: thesis: verum

end;

then A7: union F c= Cl A by ZFMISC_1:94;

now

let G be Subset of X; :: thesis: ( G in F implies G is open )
assume G in F ; :: thesis: G is open
then ex a being Point of X st
( G = Cl {a} & a in A ) ;
hence G is open by TDLAT_3:24; :: thesis: verum

end;

then F is open by TOPS_2:def 1;
then union F is open by TOPS_2:26;
then union F is closed by TDLAT_3:23;
then Cl A c= union F by A4, TOPS_1:31;
hence Cl A = union { (Cl {a}) where a is Point of X : a in A } by A7, XBOOLE_0:def 10; :: thesis: verum