:: deftheorem defines maximal_T_0 TSP_2:def 6 :
for X being non empty TopSpace
for M being Subset of X holds
( M is maximal_T_0 iff for x being Point of X ex a being Point of X st
( a in M & M /\ (MaxADSet x) = {a} ) );