theorem :: FINTOPO8:68

for NT being normal NTopSpace
for A, B being closed Subset of NT st A misses B holds
ex F being Function of NT,FMT_R^1 st
( F is continuous & ( for x being Point of NT holds
( 0 <= F . x & F . x <= 1 & ( x in A implies F . x = 0 ) & ( x in B implies F . x = 1 ) ) ) )