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 :: thesis: for C being object st C in { (Cl {a}) where a is Point of X : a in A } holds
C in bool the carrier of X
let C be object ; :: 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 :: thesis: for x being object st x in A holds
x in union F
let x be object ; :: 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:74;
A3: {a} c= Cl {a} by PRE_TOPC:18;
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 :: thesis: for C being set st C in F holds
C c= Cl A
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:31;
hence C c= Cl A by A5, PRE_TOPC:19; :: thesis: verum
end;
then A7: union F c= Cl A by ZFMISC_1:76;
now :: thesis: for G being Subset of X st G in F holds
G is open
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:22; :: thesis: verum
end;
then F is open by TOPS_2:def 1;
then union F is open by TOPS_2:19;
then union F is closed by TDLAT_3:21;
then Cl A c= union F by A4, TOPS_1:5;
hence Cl A = union { (Cl {a}) where a is Point of X : a in A } by A7; :: thesis: verum