let X be non empty TopSpace; :: thesis: for A being Subset of X holds MaxADSet A c= meet { G where G is Subset of X : ( G is open & A c= G ) }

let A be Subset of X; :: thesis: MaxADSet A c= meet { G where G is Subset of X : ( G is open & A c= G ) }

set F = { G where G is Subset of X : ( G is open & A c= G ) } ;

{ G where G is Subset of X : ( G is open & A c= G ) } c= bool the carrier of X

thus MaxADSet A c= meet { G where G is Subset of X : ( G is open & A c= G ) } by Th39; :: thesis: verum

let A be Subset of X; :: thesis: MaxADSet A c= meet { G where G is Subset of X : ( G is open & A c= G ) }

set F = { G where G is Subset of X : ( G is open & A c= G ) } ;

{ G where G is Subset of X : ( G is open & A c= G ) } c= bool the carrier of X

proof

then reconsider F = { G where G is Subset of X : ( G is open & A c= 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 & A c= G ) } or C in bool the carrier of X )

assume C in { G where G is Subset of X : ( G is open & A c= G ) } ; :: thesis: C in bool the carrier of X

then ex P being Subset of X st

( C = P & P is open & A c= 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 & A c= G ) } ; :: thesis: C in bool the carrier of X

then ex P being Subset of X st

( C = P & P is open & A c= P ) ;

hence C in bool the carrier of X ; :: thesis: verum

thus MaxADSet A c= meet { G where G is Subset of X : ( G is open & A c= G ) } by Th39; :: thesis: verum