let Y be non empty TopStruct ; :: thesis: for D being Subset of
for x being Point of st D is anti-discrete & x in D holds
D c= MaxADSet x
let D be Subset of ; :: thesis: for x being Point of st D is anti-discrete & x in D holds
D c= MaxADSet x
let x be Point of ; :: 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 : ( A is anti-discrete & x in A ) } by A1;
hence D c= MaxADSet x by ZFMISC_1:92; :: thesis: verum