theorem :: URYSOHN3:21
for T being non empty T_2 compact TopSpace
for A, B being closed Subset of T st A misses B holds
ex F being Function of T,R^1 st
( F is continuous & ( for x being Point of T holds
( 0 <= F . x & F . x <= 1 & ( x in A implies F . x = 0 ) & ( x in B implies F . x = 1 ) ) ) ) by Th20;