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

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