:: deftheorem defines MaxADSF TEX_4:def 6 :
for Y being TopStruct
for x being Point of Y holds MaxADSF x = { A where A is Subset of Y : ( A is anti-discrete & x in A ) } ;