let Y be non empty TopStruct ; :: thesis: for A being Subset of Y st { G where G is Subset of Y : ( G is open & A c= G ) } <> {} holds
MaxADSet A c= meet { G where G is Subset of Y : ( G is open & A c= G ) }
let A be Subset of Y; :: thesis: ( { G where G is Subset of Y : ( G is open & A c= G ) } <> {} implies MaxADSet A c= meet { G where G is Subset of Y : ( G is open & A c= G ) } )
set F = { G where G is Subset of Y : ( G is open & A c= G ) } ;
{ G where G is Subset of Y : ( G is open & A c= G ) } c= bool the carrier of Y

proof

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

end;

then reconsider F = { G where G is Subset of Y : ( G is open & A c= G ) } as Subset-Family of Y ;

A1: now

let C be set ; :: thesis: ( C in F implies MaxADSet A c= C )
assume C in F ; :: thesis: MaxADSet A c= C
then ex G being Subset of Y st
( G = C & G is open & A c= G ) ;
hence MaxADSet A c= C by Th40; :: thesis: verum

end;

assume { G where G is Subset of Y : ( G is open & A c= G ) } <> {} ; :: thesis: MaxADSet A c= meet { G where G is Subset of Y : ( G is open & A c= G ) }
hence MaxADSet A c= meet { G where G is Subset of Y : ( G is open & A c= G ) } by A1, SETFAM_1:5; :: thesis: verum