:: deftheorem Def1 defines Drizzle URYSOHN3:def 1 :
for T being non empty TopSpace
for A, B being Subset of T
for n being Nat st T is normal & A <> {} & A is closed & B is closed & A misses B holds
for b₅ being Function of (dyadic n),(bool the carrier of T) holds
( b₅ is Drizzle of A,B,n iff ( A c= b₅ . 0 & B = ([#] T) \ (b₅ . 1) & ( for r1, r2 being Element of dyadic n st r1 < r2 holds
( b₅ . r1 is open & b₅ . r2 is open & Cl (b₅ . r1) c= b₅ . r2 ) ) ) );