let Y be non empty TopStruct ; :: thesis: for A being Subset of Y
for x being Point of Y st x in A & A is maximal_anti-discrete holds
A = MaxADSet x
let A be Subset of Y; :: thesis: for x being Point of Y st x in A & A is maximal_anti-discrete holds
A = MaxADSet x
let x be Point of Y; :: thesis: ( x in A & A is maximal_anti-discrete implies A = MaxADSet x )
assume A1: x in A ; :: thesis: ( not A is maximal_anti-discrete or A = MaxADSet x )
assume A is maximal_anti-discrete ; :: thesis: A = MaxADSet x
then ex y being Point of Y st
( y in A & A = MaxADSet y ) by Def9;
hence A = MaxADSet x by A1, Th23; :: thesis: verum