:: deftheorem defines T_0 TSP_1:def 8 :
for Y being TopStruct
for IT being Subset of Y holds
( IT is T_0 iff for x, y being Point of Y st x in IT & y in IT & x <> y & ( for V being Subset of Y holds
( not V is open or not x in V or y in V ) ) holds
ex W being Subset of Y st
( W is open & not x in W & y in W ) );