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