:: deftheorem defines regular PRE_TOPC:def 11 :
for T being TopStruct holds
( T is regular iff for p being Point of T
for F being Subset of T st F is closed & p in F ` holds
ex G1, G2 being Subset of T st
( G1 is open & G2 is open & p in G1 & F c= G2 & G1 misses G2 ) );