let X be non empty TopSpace; :: thesis: for A being Subset of X holds Cl A = meet { F where F is Subset of X : ( F is closed & A c= F ) }

let A be Subset of X; :: thesis: Cl A = meet { F where F is Subset of X : ( F is closed & A c= F ) }

set G = { F where F is Subset of X : ( F is closed & A c= F ) } ;

A1: { F where F is Subset of X : ( F is closed & A c= F ) } c= bool the carrier of X

then reconsider G = { F where F is Subset of X : ( F is closed & A c= F ) } as non empty Subset-Family of X by A1;

A c= Cl A by PRE_TOPC:18;

then Cl A in G ;

then A3: meet G c= Cl A by SETFAM_1:3;

then Cl A c= meet G by A2, TOPS_1:5, TOPS_2:22;

hence Cl A = meet { F where F is Subset of X : ( F is closed & A c= F ) } by A3; :: thesis: verum

let A be Subset of X; :: thesis: Cl A = meet { F where F is Subset of X : ( F is closed & A c= F ) }

set G = { F where F is Subset of X : ( F is closed & A c= F ) } ;

A1: { F where F is Subset of X : ( F is closed & A c= F ) } c= bool the carrier of X

proof

[#] X in { F where F is Subset of X : ( F is closed & A c= F ) }
;
let C be object ; :: according to TARSKI:def 3 :: thesis: ( not C in { F where F is Subset of X : ( F is closed & A c= F ) } or C in bool the carrier of X )

assume C in { F where F is Subset of X : ( F is closed & A c= F ) } ; :: thesis: C in bool the carrier of X

then ex P being Subset of X st

( C = P & P is closed & A c= P ) ;

hence C in bool the carrier of X ; :: thesis: verum

end;assume C in { F where F is Subset of X : ( F is closed & A c= F ) } ; :: thesis: C in bool the carrier of X

then ex P being Subset of X st

( C = P & P is closed & A c= P ) ;

hence C in bool the carrier of X ; :: thesis: verum

then reconsider G = { F where F is Subset of X : ( F is closed & A c= F ) } as non empty Subset-Family of X by A1;

now :: thesis: for P being set st P in G holds

A c= P

then A2:
A c= meet G
by SETFAM_1:5;A c= P

let P be set ; :: thesis: ( P in G implies A c= P )

assume P in G ; :: thesis: A c= P

then ex F being Subset of X st

( F = P & F is closed & A c= F ) ;

hence A c= P ; :: thesis: verum

end;assume P in G ; :: thesis: A c= P

then ex F being Subset of X st

( F = P & F is closed & A c= F ) ;

hence A c= P ; :: thesis: verum

A c= Cl A by PRE_TOPC:18;

then Cl A in G ;

then A3: meet G c= Cl A by SETFAM_1:3;

now :: thesis: for S being Subset of X st S in G holds

S is closed

then
G is closed
by TOPS_2:def 2;S is closed

let S be Subset of X; :: thesis: ( S in G implies S is closed )

assume S in G ; :: thesis: S is closed

then ex F being Subset of X st

( F = S & F is closed & A c= F ) ;

hence S is closed ; :: thesis: verum

end;assume S in G ; :: thesis: S is closed

then ex F being Subset of X st

( F = S & F is closed & A c= F ) ;

hence S is closed ; :: thesis: verum

then Cl A c= meet G by A2, TOPS_1:5, TOPS_2:22;

hence Cl A = meet { F where F is Subset of X : ( F is closed & A c= F ) } by A3; :: thesis: verum