let Y be non empty TopSpace; :: thesis: for A being Subset of Y 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: 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

then G <> {} ;

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

let A be Subset of Y; :: 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

then reconsider G = { F where F is Subset of Y : ( F is closed & A c= F ) } as Subset-Family of Y ;
let C be object ; :: 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;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

A1: now :: thesis: for C being set st C in G holds

MaxADSet A c= C

[#] Y in G
;MaxADSet A c= C

let C be set ; :: thesis: ( C in G implies MaxADSet A c= C )

assume C in G ; :: thesis: MaxADSet A c= C

then ex F being Subset of Y st

( F = C & F is closed & A c= F ) ;

hence MaxADSet A c= C by Th40; :: thesis: verum

end;assume C in G ; :: thesis: MaxADSet A c= C

then ex F being Subset of Y st

( F = C & F is closed & A c= F ) ;

hence MaxADSet A c= C by Th40; :: thesis: verum

then G <> {} ;

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