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
proof
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;
[#] X in { F where F is Subset of X : ( F is closed & A c= F ) } ;
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
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;
then A2: A c= meet G by SETFAM_1:5;
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
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;
then G is closed by TOPS_2:def 2;
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