let Y be non empty TopStruct ; :: thesis: for D being Subset of Y

for x being Point of Y st D is anti-discrete & x in D holds

D c= MaxADSet x

let D be Subset of Y; :: thesis: for x being Point of Y st D is anti-discrete & x in D holds

D c= MaxADSet x

let x be Point of Y; :: thesis: ( D is anti-discrete & x in D implies D c= MaxADSet x )

assume A1: D is anti-discrete ; :: thesis: ( not x in D or D c= MaxADSet x )

assume x in D ; :: thesis: D c= MaxADSet x

then D in { A where A is Subset of Y : ( A is anti-discrete & x in A ) } by A1;

hence D c= MaxADSet x by ZFMISC_1:74; :: thesis: verum

for x being Point of Y st D is anti-discrete & x in D holds

D c= MaxADSet x

let D be Subset of Y; :: thesis: for x being Point of Y st D is anti-discrete & x in D holds

D c= MaxADSet x

let x be Point of Y; :: thesis: ( D is anti-discrete & x in D implies D c= MaxADSet x )

assume A1: D is anti-discrete ; :: thesis: ( not x in D or D c= MaxADSet x )

assume x in D ; :: thesis: D c= MaxADSet x

then D in { A where A is Subset of Y : ( A is anti-discrete & x in A ) } by A1;

hence D c= MaxADSet x by ZFMISC_1:74; :: thesis: verum