let T be non empty normal TopSpace; :: thesis: for A, B being closed Subset of T st A <> {} & A misses B holds
for G being Rain of A,B
for x being Real st x in DYADIC holds
ex y being Subset of T st
for n being Nat st x in dyadic n holds
y = (G . n) . x

let A, B be closed Subset of T; :: thesis: ( A <> {} & A misses B implies for G being Rain of A,B
for x being Real st x in DYADIC holds
ex y being Subset of T st
for n being Nat st x in dyadic n holds
y = (G . n) . x )

assume A1: ( A <> {} & A misses B ) ; :: thesis: for G being Rain of A,B
for x being Real st x in DYADIC holds
ex y being Subset of T st
for n being Nat st x in dyadic n holds
y = (G . n) . x

let G be Rain of A,B; :: thesis: for x being Real st x in DYADIC holds
ex y being Subset of T st
for n being Nat st x in dyadic n holds
y = (G . n) . x

let x be Real; :: thesis: ( x in DYADIC implies ex y being Subset of T st
for n being Nat st x in dyadic n holds
y = (G . n) . x )

assume A2: x in DYADIC ; :: thesis: ex y being Subset of T st
for n being Nat st x in dyadic n holds
y = (G . n) . x

reconsider s = inf_number_dyadic x as Nat ;
G . s is Drizzle of A,B,s by ;
then reconsider y = (G . s) . x as Subset of T by ;
take y ; :: thesis: for n being Nat st x in dyadic n holds
y = (G . n) . x

let n be Nat; :: thesis: ( x in dyadic n implies y = (G . n) . x )
assume x in dyadic n ; :: thesis: y = (G . n) . x
then consider m being Nat such that
A3: n = s + m by ;
thus y = (G . n) . x by A1, A2, A3, Th8; :: thesis: verum