let X be non empty TopSpace; :: thesis: for x being Point of X holds MaxADSet x c= meet { F where F is Subset of X : ( F is closed & x in F ) }
let x be Point of X; :: thesis: MaxADSet x c= meet { F where F is Subset of X : ( F is closed & x in F ) }
set G = { F where F is Subset of X : ( F is closed & x in F ) } ;
[#] X in { F where F is Subset of X : ( F is closed & x in F ) } ;
then A1: { F where F is Subset of X : ( F is closed & x in F ) } <> {} ;
{ F where F is Subset of X : ( F is closed & x in 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 & x in F ) } or C in bool the carrier of X )
assume C in { F where F is Subset of X : ( F is closed & x in F ) } ; :: thesis: C in bool the carrier of X
then ex P being Subset of X st
( C = P & P is closed & x in 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 & x in F ) } as Subset-Family of X ;

now :: thesis: for C being set st C in G holds
MaxADSet x c= C

let C be set ; :: thesis: ( C in G implies MaxADSet x c= C )
assume C in G ; :: thesis: MaxADSet x c= C
then ex F being Subset of X st
( F = C & F is closed & x in F ) ;
hence MaxADSet x c= C by Th23; :: thesis: verum

end;

hence MaxADSet x c= meet { F where F is Subset of X : ( F is closed & x in F ) } by A1, SETFAM_1:5; :: thesis: verum