:: deftheorem Def13 defines normal FINTOPO8:def 13 :
for NT being NTopSpace holds
( NT is normal iff for A, B being closed Subset of NT st A misses B holds
ex V being a_neighborhood of A ex W being a_neighborhood of B st V misses W );