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

ex G being Function of (dyadic 0),(bool the carrier of T) st

( A c= G . 0 & B = ([#] T) \ (G . 1) & ( for r1, r2 being Element of dyadic 0 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 ex G being Function of (dyadic 0),(bool the carrier of T) st

( A c= G . 0 & B = ([#] T) \ (G . 1) & ( for r1, r2 being Element of dyadic 0 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: ex G being Function of (dyadic 0),(bool the carrier of T) st

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

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

reconsider G1 = ([#] T) \ B as Subset of T ;

A3: G1 = B ` by SUBSET_1:def 4;

then A4: G1 is open by TOPS_1:3;

A \ B c= G1 by XBOOLE_1:33;

then A c= G1 by A2, XBOOLE_1:83;

then consider G0 being Subset of T such that

A5: G0 is open and

A6: A c= G0 and

A7: Cl G0 c= G1 by A1, A4, URYSOHN1:23;

defpred S_{1}[ set , set ] means ( ( $1 = 0 implies $2 = G0 ) & ( $1 = 1 implies $2 = G1 ) );

A8: for x being Element of dyadic 0 ex y being Subset of T st S_{1}[x,y]

for x being Element of dyadic 0 holds S_{1}[x,F . x]
from FUNCT_2:sch 3(A8);

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

A11: for x being Element of dyadic 0 holds S_{1}[x,F . x]
;

A12: for r1, r2 being Element of dyadic 0 st r1 < r2 holds

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

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

1 in dyadic 0 by TARSKI:def 2, URYSOHN1:2;

then ( 0 in dyadic 0 & F . 1 = G1 ) by A11, TARSKI:def 2, URYSOHN1:2;

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

( F . r1 is open & F . r2 is open & Cl (F . r1) c= F . r2 ) ) ) by A6, A11, A12, PRE_TOPC:3; :: thesis: verum

ex G being Function of (dyadic 0),(bool the carrier of T) st

( A c= G . 0 & B = ([#] T) \ (G . 1) & ( for r1, r2 being Element of dyadic 0 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 ex G being Function of (dyadic 0),(bool the carrier of T) st

( A c= G . 0 & B = ([#] T) \ (G . 1) & ( for r1, r2 being Element of dyadic 0 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: ex G being Function of (dyadic 0),(bool the carrier of T) st

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

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

reconsider G1 = ([#] T) \ B as Subset of T ;

A3: G1 = B ` by SUBSET_1:def 4;

then A4: G1 is open by TOPS_1:3;

A \ B c= G1 by XBOOLE_1:33;

then A c= G1 by A2, XBOOLE_1:83;

then consider G0 being Subset of T such that

A5: G0 is open and

A6: A c= G0 and

A7: Cl G0 c= G1 by A1, A4, URYSOHN1:23;

defpred S

A8: for x being Element of dyadic 0 ex y being Subset of T st S

proof

ex F being Function of (dyadic 0),(bool the carrier of T) st
let x be Element of dyadic 0; :: thesis: ex y being Subset of T st S_{1}[x,y]

end;per cases
( x = 0 or x = 1 )
by TARSKI:def 2, URYSOHN1:2;

end;

for x being Element of dyadic 0 holds S

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

A11: for x being Element of dyadic 0 holds S

A12: for r1, r2 being Element of dyadic 0 st r1 < r2 holds

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

proof

take
F
; :: thesis: ( A c= F . 0 & B = ([#] T) \ (F . 1) & ( for r1, r2 being Element of dyadic 0 st r1 < r2 holds
let r1, r2 be Element of dyadic 0; :: thesis: ( r1 < r2 implies ( F . r1 is open & F . r2 is open & Cl (F . r1) c= F . r2 ) )

A13: ( r1 = 0 or r1 = 1 ) by TARSKI:def 2, URYSOHN1:2;

A14: ( r2 = 0 or r2 = 1 ) by TARSKI:def 2, URYSOHN1:2;

assume A15: r1 < r2 ; :: thesis: ( F . r1 is open & F . r2 is open & Cl (F . r1) c= F . r2 )

then F . 1 = G1 by A11, A14, URYSOHN1:2;

hence ( F . r1 is open & F . r2 is open & Cl (F . r1) c= F . r2 ) by A3, A5, A7, A11, A15, A13, A14, TOPS_1:3; :: thesis: verum

end;A13: ( r1 = 0 or r1 = 1 ) by TARSKI:def 2, URYSOHN1:2;

A14: ( r2 = 0 or r2 = 1 ) by TARSKI:def 2, URYSOHN1:2;

assume A15: r1 < r2 ; :: thesis: ( F . r1 is open & F . r2 is open & Cl (F . r1) c= F . r2 )

then F . 1 = G1 by A11, A14, URYSOHN1:2;

hence ( F . r1 is open & F . r2 is open & Cl (F . r1) c= F . r2 ) by A3, A5, A7, A11, A15, A13, A14, TOPS_1:3; :: thesis: verum

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

1 in dyadic 0 by TARSKI:def 2, URYSOHN1:2;

then ( 0 in dyadic 0 & F . 1 = G1 ) by A11, TARSKI:def 2, URYSOHN1:2;

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

( F . r1 is open & F . r2 is open & Cl (F . r1) c= F . r2 ) ) ) by A6, A11, A12, PRE_TOPC:3; :: thesis: verum