:: deftheorem Def4 defines Tempest URYSOHN3:def 4 :
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 R being Rain of A,B
for b₅ being Function of DOM,(bool the carrier of T) holds
( b₅ = Tempest R iff for x being Real st x in DOM holds
( ( x in halfline 0 implies b₅ . x = {} ) & ( x in right_open_halfline 1 implies b₅ . x = the carrier of T ) & ( x in DYADIC implies for n being Nat st x in dyadic n holds
b₅ . x = (R . n) . x ) ) );