:: deftheorem defines T_0 TSP_1:def 4 :
for Y being TopStruct holds
( Y is T_0 iff ( Y is empty or for x, y being Point of Y holds
( not x <> y or ex E being Subset of Y st
( E is closed & x in E & not y in E ) or ex F being Subset of Y st
( F is closed & not x in F & y in F ) ) ) );