:: deftheorem defines maximal_discrete TEX_2:def 5 :
for Y being TopStruct
for IT being Subset of Y holds
( IT is maximal_discrete iff ( IT is discrete & ( for D being Subset of Y st D is discrete & IT c= D holds
IT = D ) ) );