:: deftheorem defines maximal_discrete TEX_2:def 6 :
for Y being non empty TopStruct
for IT being SubSpace of Y holds
( IT is maximal_discrete iff for A being Subset of Y st A = the carrier of IT holds
A is maximal_discrete );