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 that
A1: F is closed and
A2: x in F ; :: thesis: MaxADSet x c= F
{x} c= MaxADSet x by Th12;
then A3: x in MaxADSet x by ZFMISC_1:31;
MaxADSet x is maximal_anti-discrete by Th20;
then MaxADSet x is anti-discrete ;
hence MaxADSet x c= F by A1, A2, A3; :: thesis: verum