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

proof

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

end;

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

now

let C be set ; :: thesis: ( C in G implies MaxADSet A c= C )
assume C in G ; :: thesis: MaxADSet A c= C
then consider F being Subset of Y such that
A2: F = C and
A3: ( F is closed & A c= F ) ;
thus MaxADSet A c= C by A2, A3, Th42; :: thesis: verum

end;

hence MaxADSet A c= meet { F where F is Subset of Y : ( F is closed & A c= F ) } by A1, SETFAM_1:6; :: thesis: verum