:: deftheorem defines T_0 TSP_1:def 11 :
for X being non empty TopSpace
for A being Subset of X holds
( A is T_0 iff for x, y being Point of X st x in A & y in A & x <> y & x in Cl {y} holds
not y in Cl {x} );