theorem Th4: :: URYSOHN3:4

for T being non empty normal TopSpace
for A, B being closed Subset of T st A <> {} & A misses B holds
ex F being Functional_Sequence of DYADIC,(bool the carrier of T) st
for n being Nat holds
( F . n is Drizzle of A,B,n & ( for r being Element of dom (F . n) holds (F . n) . r = (F . (n + 1)) . r ) )