:: deftheorem defines T_0 TSP_2:def 1 :
for X being non empty TopSpace
for A being Subset of X holds
( A is T_0 iff for a, b being Point of X st a in A & b in A & a <> b holds
MaxADSet a misses MaxADSet b );