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 that
A1: G is open and
A2: x in G ; :: thesis: MaxADSet x c= G
{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= G by A1, A2, A3; :: thesis: verum