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 Element of 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 Element of 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 Element of 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 Element of 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 Element of 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 Element of NAT st x in dyadic n holds
y = (G . n) . x
reconsider s = inf_number_dyadic x as Element of NAT ;
G . s is Drizzle of A,B,s by A1, Def2;
then reconsider y = (G . s) . x as Subset of T by A2, Th6, FUNCT_2:7;
take y ; :: thesis: for n being Element of NAT st x in dyadic n holds
y = (G . n) . x
let n be Element of 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 Th8, NAT_1:10;
m in NAT by ORDINAL1:def 13;
hence y = (G . n) . x by A1, A2, A3, Th9; :: thesis: verum