let Y be non empty TopStruct ; :: thesis: for F being Subset of Y
for x being Point of Y st F is closed & x in F holds
MaxADSet x c= F
let F be Subset of Y; :: thesis: for x being Point of Y st F is closed & x in F holds
MaxADSet x c= F
let x be Point of Y; :: thesis: ( F is closed & x in F implies MaxADSet x c= F )
assume A1: ( F is closed & x in F ) ; :: thesis: MaxADSet x c= F
MaxADSet x is maximal_anti-discrete by Th22;
then A2: MaxADSet x is anti-discrete by Def7;
{x} c= MaxADSet x by Th14;
then x in MaxADSet x by ZFMISC_1:37;
hence MaxADSet x c= F by A1, A2, Def2; :: thesis: verum