for T being non empty normal TopSpace
for A, B being closed Subset of T st A <> {} & A misses B holds
for G being Rain of A,B holds
( Thunder G is continuous & ( for x being Point of T holds
( 0 <= (Thunder G) . x & (Thunder G) . x <= 1 & ( x in A implies (Thunder G) . x = 0 ) & ( x in B implies (Thunder G) . x = 1 ) ) ) )