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
for r being Real st r in DYADIC \/ (right_open_halfline 1) & 0 < r holds
for p being Point of T st p in (Tempest G) . r holds
(Thunder G) . p <= r