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 (),(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 (),(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 (),(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 ;
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 ;
defpred S1[ 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 S1[x,y]
proof
let x be Element of dyadic 0; :: thesis: ex y being Subset of T st S1[x,y]
per cases ( x = 0 or x = 1 ) by ;
suppose A9: x = 0 ; :: thesis: ex y being Subset of T st S1[x,y]
take G0 ; :: thesis: S1[x,G0]
thus S1[x,G0] by A9; :: thesis: verum
end;
suppose A10: x = 1 ; :: thesis: ex y being Subset of T st S1[x,y]
take G1 ; :: thesis: S1[x,G1]
thus S1[x,G1] by A10; :: thesis: verum
end;
end;
end;
ex F being Function of (),(bool the carrier of T) st
for x being Element of dyadic 0 holds S1[x,F . x] from then consider F being Function of (),(bool the carrier of T) such that
A11: for x being Element of dyadic 0 holds S1[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 )
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 ) )
A13: ( r1 = 0 or r1 = 1 ) by ;
A14: ( r2 = 0 or r2 = 1 ) by ;
assume A15: r1 < r2 ; :: thesis: ( F . r1 is open & F . r2 is open & Cl (F . r1) c= F . r2 )
then F . 1 = G1 by ;
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;
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 ) ) )

1 in dyadic 0 by ;
then ( 0 in dyadic 0 & F . 1 = G1 ) by ;
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 ; :: thesis: verum