let X be non empty TopSpace; :: thesis: for x being Point of X holds MaxADSet x c= Cl {x}
let x be Point of X; :: thesis: MaxADSet x c= Cl {x}
Cl {x} = meet { F where F is Subset of X : ( F is closed & x in F ) } by Th2;
hence MaxADSet x c= Cl {x} by Th47; :: thesis: verum