:: deftheorem Def5 defines Rainbow URYSOHN3:def 5 :
for T being non empty TopSpace
for A, B being Subset of T
for G being Rain of A,B
for p being Point of T
for b₆ being Subset of ExtREAL holds
( b₆ = Rainbow (p,G) iff for x being set holds
( x in b₆ iff ( x in DYADIC & ( for s being Real st s = x holds
not p in (Tempest G) . s ) ) ) );