:: deftheorem defines maximal_anti-discrete TEX_4:def 16 :
for Y being non empty TopStruct
for IT being SubSpace of Y holds
( IT is maximal_anti-discrete iff ( IT is anti-discrete & ( for Y0 being SubSpace of Y st Y0 is anti-discrete & the carrier of IT c= the carrier of Y0 holds
the carrier of IT = the carrier of Y0 ) ) );