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

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