let T be non empty normal TopSpace; :: thesis: for A, B being closed Subset of T st A <> {} & A misses B holds

for n being Nat

for G being Drizzle of A,B,n ex F being Drizzle of A,B,n + 1 st

for r being Element of dyadic (n + 1) st r in dyadic n holds

F . r = G . r

let A, B be closed Subset of T; :: thesis: ( A <> {} & A misses B implies for n being Nat

for G being Drizzle of A,B,n ex F being Drizzle of A,B,n + 1 st

for r being Element of dyadic (n + 1) st r in dyadic n holds

F . r = G . r )

assume that

A1: A <> {} and

A2: A misses B ; :: thesis: for n being Nat

for G being Drizzle of A,B,n ex F being Drizzle of A,B,n + 1 st

for r being Element of dyadic (n + 1) st r in dyadic n holds

F . r = G . r

let n be Nat; :: thesis: for G being Drizzle of A,B,n ex F being Drizzle of A,B,n + 1 st

for r being Element of dyadic (n + 1) st r in dyadic n holds

F . r = G . r

let G be Drizzle of A,B,n; :: thesis: ex F being Drizzle of A,B,n + 1 st

for r being Element of dyadic (n + 1) st r in dyadic n holds

F . r = G . r

A3: for r1, r2 being Element of dyadic n st r1 < r2 holds

( G . r1 is open & G . r2 is open & Cl (G . r1) c= G . r2 ) by A1, A2, Def1;

( A c= G . 0 & B = ([#] T) \ (G . 1) ) by A1, A2, Def1;

then consider F being Function of (dyadic (n + 1)),(bool the carrier of T) such that

A4: ( A c= F . 0 & B = ([#] T) \ (F . 1) ) and

A5: for r1, r2, r being Element of dyadic (n + 1) st r1 < r2 holds

( F . r1 is open & F . r2 is open & Cl (F . r1) c= F . r2 & ( r in dyadic n implies F . r = G . r ) ) by A1, A3, URYSOHN1:24;

for r1, r2 being Element of dyadic (n + 1) st r1 < r2 holds

( F . r1 is open & F . r2 is open & Cl (F . r1) c= F . r2 ) by A5;

then reconsider F = F as Drizzle of A,B,n + 1 by A1, A2, A4, Def1;

take F ; :: thesis: for r being Element of dyadic (n + 1) st r in dyadic n holds

F . r = G . r

let r be Element of dyadic (n + 1); :: thesis: ( r in dyadic n implies F . r = G . r )

A6: ( 0 in dyadic (n + 1) & 1 in dyadic (n + 1) ) by URYSOHN1:6;

assume r in dyadic n ; :: thesis: F . r = G . r

hence F . r = G . r by A5, A6; :: thesis: verum

for n being Nat

for G being Drizzle of A,B,n ex F being Drizzle of A,B,n + 1 st

for r being Element of dyadic (n + 1) st r in dyadic n holds

F . r = G . r

let A, B be closed Subset of T; :: thesis: ( A <> {} & A misses B implies for n being Nat

for G being Drizzle of A,B,n ex F being Drizzle of A,B,n + 1 st

for r being Element of dyadic (n + 1) st r in dyadic n holds

F . r = G . r )

assume that

A1: A <> {} and

A2: A misses B ; :: thesis: for n being Nat

for G being Drizzle of A,B,n ex F being Drizzle of A,B,n + 1 st

for r being Element of dyadic (n + 1) st r in dyadic n holds

F . r = G . r

let n be Nat; :: thesis: for G being Drizzle of A,B,n ex F being Drizzle of A,B,n + 1 st

for r being Element of dyadic (n + 1) st r in dyadic n holds

F . r = G . r

let G be Drizzle of A,B,n; :: thesis: ex F being Drizzle of A,B,n + 1 st

for r being Element of dyadic (n + 1) st r in dyadic n holds

F . r = G . r

A3: for r1, r2 being Element of dyadic n st r1 < r2 holds

( G . r1 is open & G . r2 is open & Cl (G . r1) c= G . r2 ) by A1, A2, Def1;

( A c= G . 0 & B = ([#] T) \ (G . 1) ) by A1, A2, Def1;

then consider F being Function of (dyadic (n + 1)),(bool the carrier of T) such that

A4: ( A c= F . 0 & B = ([#] T) \ (F . 1) ) and

A5: for r1, r2, r being Element of dyadic (n + 1) st r1 < r2 holds

( F . r1 is open & F . r2 is open & Cl (F . r1) c= F . r2 & ( r in dyadic n implies F . r = G . r ) ) by A1, A3, URYSOHN1:24;

for r1, r2 being Element of dyadic (n + 1) st r1 < r2 holds

( F . r1 is open & F . r2 is open & Cl (F . r1) c= F . r2 ) by A5;

then reconsider F = F as Drizzle of A,B,n + 1 by A1, A2, A4, Def1;

take F ; :: thesis: for r being Element of dyadic (n + 1) st r in dyadic n holds

F . r = G . r

let r be Element of dyadic (n + 1); :: thesis: ( r in dyadic n implies F . r = G . r )

A6: ( 0 in dyadic (n + 1) & 1 in dyadic (n + 1) ) by URYSOHN1:6;

assume r in dyadic n ; :: thesis: F . r = G . r

hence F . r = G . r by A5, A6; :: thesis: verum