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 A1: ( A <> {} & 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 ;
A2: G1 = B ` by SUBSET_1:def 5;
then A3: G1 is open by TOPS_1:29;
A \ B c= G1 by XBOOLE_1:33;
then A c= G1 by A1, XBOOLE_1:83;
then consider G0 being Subset of T such that
A4: ( G0 is open & A c= G0 & Cl G0 c= G1 ) by A1, A3, URYSOHN1:31;
defpred S₁[ set , set ] means ( ( $1 = 0 implies $2 = G0 ) & ( $1 = 1 implies $2 = G1 ) );
A5: for x being Element of dyadic 0 ex y being Subset of T st S₁[x,y]

proof

let x be Element of dyadic 0 ; :: thesis: ex y being Subset of T st S₁[x,y]

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

suppose A6: x = 0 ; :: thesis: ex y being Subset of T st S₁[x,y]

take G0 ; :: thesis: S₁[x,G0]
thus S₁[x,G0] by A6; :: thesis: verum

end;

suppose A7: x = 1 ; :: thesis: ex y being Subset of T st S₁[x,y]

take G1 ; :: thesis: S₁[x,G1]
thus S₁[x,G1] by A7; :: thesis: verum

end;

end;

end;

ex F being Function of (dyadic 0 ),(bool the carrier of T) st
for x being Element of dyadic 0 holds S₁[x,F . x] from FUNCT_2:sch 3(A5);
then consider F being Function of (dyadic 0 ),(bool the carrier of T) such that
A8: for x being Element of dyadic 0 holds S₁[x,F . x] ;
take F ; :: thesis: ( 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 ) ) )
A9: ( F . 0 = G0 & F . 1 = G1 )

proof

( 0 in dyadic 0 & 1 in dyadic 0 ) by TARSKI:def 2, URYSOHN1:6;
hence ( F . 0 = G0 & F . 1 = G1 ) by A8; :: thesis: verum

end;

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

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 ) )
assume A10: r1 < r2 ; :: thesis: ( F . r1 is open & F . r2 is open & Cl (F . r1) c= F . r2 )
A11: ( ( r1 = 0 or r1 = 1 ) & ( r2 = 0 or r2 = 1 ) ) by TARSKI:def 2, URYSOHN1:6;
then ( F . 0 = G0 & F . 1 = G1 ) by A8, A10;
hence ( F . r1 is open & F . r2 is open & Cl (F . r1) c= F . r2 ) by A2, A4, A10, A11, TOPS_1:29; :: thesis: verum

end;

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 A4, A9, PRE_TOPC:22; :: thesis: verum