:: deftheorem defines T_1 URYSOHN1:def 7 :
for T being TopSpace holds
( T is T_1 iff for p, q being Point of T st not p = q holds
ex W, V being Subset of T st
( W is open & V is open & p in W & not q in W & q in V & not p in V ) );