:: deftheorem defines regular COMPTS_1:def 2 :
for T being non empty TopSpace holds
( T is regular iff for p being Point of T
for P being Subset of T st P <> {} & P is closed & p in P ` holds
ex W, V being Subset of T st
( W is open & V is open & p in W & P c= V & W misses V ) );