theorem :: URYSOHN1:24

for T being non empty TopSpace st T is normal holds
for A, B being closed Subset of T st A <> {} holds
for n being Nat
for G being Function of (dyadic n),(bool the carrier of T) st A c= G . 0 & B = ([#] T) \ (G . 1) & ( for r1, r2 being Element of dyadic n st r1 < r2 holds
( G . r1 is open & G . r2 is open & Cl (G . r1) c= G . r2 ) ) holds
ex F being Function of (dyadic (n + 1)),(bool the carrier of T) st
( A c= F . 0 & B = ([#] T) \ (F . 1) & ( for r1, r2, r being Element of dyadic (n + 1) st r1 < r2 holds
( F . r1 is open & F . r2 is open & Cl (F . r1) c= F . r2 & ( r in dyadic n implies F . r = G . r ) ) ) )