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 ) } ;

[#] X in { G where G is Subset of X : ( G is open & x in G ) } ;

then A1: { 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

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 ) } ;

[#] X in { G where G is Subset of X : ( G is open & x in G ) } ;

then A1: { 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

then reconsider F = { G where G is Subset of X : ( G is open & x in G ) } as Subset-Family of X ;
let C be object ; :: 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;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

now :: thesis: for C being set st C in F holds

MaxADSet x c= C

hence
MaxADSet x c= meet { G where G is Subset of X : ( G is open & x in G ) }
by A1, SETFAM_1:5; :: thesis: verumMaxADSet x c= C

let C be set ; :: thesis: ( C in F implies MaxADSet x c= C )

assume C in F ; :: thesis: MaxADSet x c= C

then ex G being Subset of X st

( G = C & G is open & x in G ) ;

hence MaxADSet x c= C by Th24; :: thesis: verum

end;assume C in F ; :: thesis: MaxADSet x c= C

then ex G being Subset of X st

( G = C & G is open & x in G ) ;

hence MaxADSet x c= C by Th24; :: thesis: verum