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