:: deftheorem defines maximal_anti-discrete TEX_4:def 7 :
for Y being TopStruct
for IT being Subset of Y holds
( IT is maximal_anti-discrete iff ( IT is anti-discrete & ( for D being Subset of Y st D is anti-discrete & IT c= D holds
IT = D ) ) );