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