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

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 consider C being Subset of Y such that
A1: C = A and
A2: C is anti-discrete and
x in C ;
thus A is anti-discrete by A1, A2; :: thesis: verum

end;

hence MaxADSF x is anti-discrete-set-family by Def5; :: thesis: verum