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 consider y being Point of Y such that
y in A and
A2: A = MaxADSet y by Def9;
thus A = MaxADSet x by A1, A2, Th23; :: thesis: verum