let X be non empty TopSpace; :: thesis: for x being Point of X holds MaxADSet x c= meet { G where G is Subset of X : ( G is open & x in G ) }
let x be Point of X; :: thesis: MaxADSet x c= meet { G where G is Subset of X : ( G is open & x in G ) }
set F = { G where G is Subset of X : ( G is open & x in G ) } ;
{ G where G is Subset of X : ( G is open & x in G ) } c= bool the carrier of X

proof

let C be set ; :: according to TARSKI:def 3 :: thesis: ( not C in { G where G is Subset of X : ( G is open & x in G ) } or C in bool the carrier of X )
assume C in { G where G is Subset of X : ( G is open & x in G ) } ; :: thesis: C in bool the carrier of X
then ex P being Subset of X st
( C = P & P is open & x in P ) ;
hence C in bool the carrier of X ; :: thesis: verum

end;

then reconsider F = { G where G is Subset of X : ( G is open & x in G ) } as Subset-Family of X ;

now

let C be set ; :: thesis: ( C in F implies MaxADSet x c= C )
assume C in F ; :: thesis: MaxADSet x c= C
then consider G being Subset of X such that
A1: G = C and
A2: ( G is open & x in G ) ;
thus MaxADSet x c= C by A1, A2, Th26; :: thesis: verum

end;

hence MaxADSet x c= meet { G where G is Subset of X : ( G is open & x in G ) } by SETFAM_1:6; :: thesis: verum