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