let Y be non empty TopStruct ; :: thesis: for x being Point of Y holds MaxADSF x is anti-discrete-set-family
let x be Point of Y; :: thesis: MaxADSF x is anti-discrete-set-family
now :: thesis: for A being Subset of Y st A in MaxADSF x holds
A is anti-discrete
let A be Subset of Y; :: thesis: ( A in MaxADSF x implies A is anti-discrete )
assume A in MaxADSF x ; :: thesis: A is anti-discrete
then ex C being Subset of Y st
( C = A & C is anti-discrete & x in C ) ;
hence A is anti-discrete ; :: thesis: verum
end;
hence MaxADSF x is anti-discrete-set-family ; :: thesis: verum