theorem Th1: :: URYSOHN3:1

for T being non empty normal TopSpace
for A, B being closed Subset of T st A <> {} & A misses B holds
for n being Nat ex 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 ) ) )