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 ex G being Function of (dyadic n),(bool the carrier of T) st

( A c= G . 0 & B = ([#] T) \ (G . 1) & ( 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 ) ) )

let A, B be closed Subset of T; :: thesis: ( A <> {} & A misses B implies for n being Nat ex G being Function of (dyadic n),(bool the carrier of T) st

( A c= G . 0 & B = ([#] T) \ (G . 1) & ( 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 ) ) ) )

assume that

A1: A <> {} and

A2: A misses B ; :: thesis: for n being Nat ex G being Function of (dyadic n),(bool the carrier of T) st

( A c= G . 0 & B = ([#] T) \ (G . 1) & ( 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 ) ) )

defpred S_{1}[ Nat] means ex G being Function of (dyadic $1),(bool the carrier of T) st

( A c= G . 0 & B = ([#] T) \ (G . 1) & ( for r1, r2 being Element of dyadic $1 st r1 < r2 holds

( G . r1 is open & G . r2 is open & Cl (G . r1) c= G . r2 ) ) );

A3: for n being Nat st S_{1}[n] holds

S_{1}[n + 1]
_{1}[ 0 ]
by A1, A2, Lm1;

thus for n being Nat holds S_{1}[n]
from NAT_1:sch 2(A6, A3); :: thesis: verum

for n being Nat ex G being Function of (dyadic n),(bool the carrier of T) st

( A c= G . 0 & B = ([#] T) \ (G . 1) & ( 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 ) ) )

let A, B be closed Subset of T; :: thesis: ( A <> {} & A misses B implies for n being Nat ex G being Function of (dyadic n),(bool the carrier of T) st

( A c= G . 0 & B = ([#] T) \ (G . 1) & ( 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 ) ) ) )

assume that

A1: A <> {} and

A2: A misses B ; :: thesis: for n being Nat ex G being Function of (dyadic n),(bool the carrier of T) st

( A c= G . 0 & B = ([#] T) \ (G . 1) & ( 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 ) ) )

defpred S

( A c= G . 0 & B = ([#] T) \ (G . 1) & ( for r1, r2 being Element of dyadic $1 st r1 < r2 holds

( G . r1 is open & G . r2 is open & Cl (G . r1) c= G . r2 ) ) );

A3: for n being Nat st S

S

proof

A6:
S
let n be Nat; :: thesis: ( S_{1}[n] implies S_{1}[n + 1] )

given G being Function of (dyadic n),(bool the carrier of T) such that A4: ( A c= G . 0 & B = ([#] T) \ (G . 1) & ( 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 ) ) ) ; :: thesis: S_{1}[n + 1]

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

A5: ( A c= F . 0 & B = ([#] T) \ (F . 1) & ( 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, A4, URYSOHN1:24;

take F ; :: thesis: ( A c= F . 0 & B = ([#] T) \ (F . 1) & ( 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 ) ) )

thus ( A c= F . 0 & B = ([#] T) \ (F . 1) & ( 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; :: thesis: verum

end;given G being Function of (dyadic n),(bool the carrier of T) such that A4: ( A c= G . 0 & B = ([#] T) \ (G . 1) & ( 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 ) ) ) ; :: thesis: S

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

A5: ( A c= F . 0 & B = ([#] T) \ (F . 1) & ( 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, A4, URYSOHN1:24;

take F ; :: thesis: ( A c= F . 0 & B = ([#] T) \ (F . 1) & ( 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 ) ) )

thus ( A c= F . 0 & B = ([#] T) \ (F . 1) & ( 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; :: thesis: verum

thus for n being Nat holds S