let Y be non empty TopStruct ; :: thesis: for G being Subset of Y
for x being Point of Y st G is open & x in G holds
MaxADSet x c= G
let G be Subset of Y; :: thesis: for x being Point of Y st G is open & x in G holds
MaxADSet x c= G
let x be Point of Y; :: thesis: ( G is open & x in G implies MaxADSet x c= G )
assume A1: ( G is open & x in G ) ; :: thesis: MaxADSet x c= G
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= G by A1, A2, Def1; :: thesis: verum