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 A1, Def2;

then reconsider y = (G . s) . x as Subset of T by A2, Th5, FUNCT_2:5;

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 Th7, NAT_1:10;

thus y = (G . n) . x by A1, A2, A3, Th8; :: thesis: verum

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 A1, Def2;

then reconsider y = (G . s) . x as Subset of T by A2, Th5, FUNCT_2:5;

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 Th7, NAT_1:10;

thus y = (G . n) . x by A1, A2, A3, Th8; :: thesis: verum