let X be non empty TopSpace; :: thesis: for A being Subset of X holds MaxADSet A c= meet { F where F is Subset of X : ( F is closed & A c= F ) }
let A be Subset of X; :: thesis: MaxADSet A c= 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 ) } ;
{ 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;

then reconsider G = { F where F is Subset of X : ( F is closed & A c= F ) } as Subset-Family of X ;
[#] X in G ;
hence MaxADSet A c= meet { F where F is Subset of X : ( F is closed & A c= F ) } by Th41; :: thesis: verum