let X be non empty TopSpace; :: thesis: for A being Subset of X holds MaxADSet A c= Cl A
let A be Subset of X; :: thesis: MaxADSet A c= Cl A
Cl A = meet { F where F is Subset of X : ( F is closed & A c= F ) } by Th1;
hence MaxADSet A c= Cl A by Th58; :: thesis: verum