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