:: deftheorem defines maximal_T_0 TSP_2:def 5 :
for X being non empty TopSpace
for M being Subset of X holds
( M is maximal_T_0 iff ( M is T_0 & MaxADSet M = the carrier of X ) );