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