:: deftheorem Def2 defines Rain URYSOHN3:def 2 :
for T being non empty TopSpace
for A, B being Subset of T st T is normal & A <> {} & A is closed & B is closed & A misses B holds
for b₄ being Functional_Sequence of DYADIC,(bool the carrier of T) holds
( b₄ is Rain of A,B iff for n being Nat holds
( b₄ . n is Drizzle of A,B,n & ( for r being Element of dom (b₄ . n) holds (b₄ . n) . r = (b₄ . (n + 1)) . r ) ) );