:: deftheorem defines normal COMPTS_1:def 3 :
for T being non empty TopSpace holds
( T is normal iff for W, V being Subset of T st W <> {} & V <> {} & W is closed & V is closed & W misses V holds
ex P, Q being Subset of T st
( P is open & Q is open & W c= P & V c= Q & P misses Q ) );