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