:: deftheorem defines T_0 TSP_2:def 2 :
for X being non empty TopSpace
for A being Subset of X holds
( A is T_0 iff for a being Point of X st a in A holds
A /\ (MaxADSet a) = {a} );