:: deftheorem Def6 defines Thunder URYSOHN3:def 6 :
for T being non empty TopSpace
for A, B being Subset of T
for R being Rain of A,B
for b₅ being Function of T,R^1 holds
( b₅ = Thunder R iff for p being Point of T holds
( ( Rainbow (p,R) = {} implies b₅ . p = 0 ) & ( for S being non empty Subset of ExtREAL st S = Rainbow (p,R) holds
b₅ . p = sup S ) ) );