:: deftheorem defines T_0 PRE_TOPC:def 8 :
for T being TopStruct holds
( T is T_0 iff for x, y being Point of T st ( for G being Subset of T st G is open holds
( x in G iff y in G ) ) holds
x = y );