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 } ;
{ (Cl {a}) where a is Point of X : a in A } c= bool the carrier of X

proof

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 consider a being Point of X such that
A1: C = Cl {a} and
a in A ;
thus C in bool the carrier of X by A1; :: thesis: verum

end;

hence { (Cl {a}) where a is Point of X : a in A } c= bool the carrier of X by TARSKI:def 3; :: thesis: verum

end;

then reconsider F = { (Cl {a}) where a is Point of X : a in A } as Subset-Family of X ;
reconsider F = F as Subset-Family of X ;
A2: A c= union F

proof

now

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

end;

hence A c= union F by TARSKI:def 3; :: thesis: verum

end;

F is open

proof

now

let G be Subset of X; :: thesis: ( G in F implies G is open )
assume G in F ; :: thesis: G is open
then consider a being Point of X such that
A5: G = Cl {a} and
a in A ;
thus G is open by A5, TDLAT_3:24; :: thesis: verum

end;

hence F is open by TOPS_2:def 1; :: thesis: verum

end;

then union F is open by TOPS_2:26;
then union F is closed by TDLAT_3:23;
then A6: Cl A c= union F by A2, TOPS_1:31;
union F c= Cl A

proof

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
A7: C = Cl {a} and
A8: a in A ;
{a} c= A by A8, ZFMISC_1:37;
hence C c= Cl A by A7, PRE_TOPC:49; :: thesis: verum

end;

hence union F c= Cl A by ZFMISC_1:94; :: thesis: verum

end;

hence Cl A = union { (Cl {a}) where a is Point of X : a in A } by A6, XBOOLE_0:def 10; :: thesis: verum