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 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 TARSKI:def 2, URYSOHN1:2;
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 (dyadic 0),(bool the carrier of T) st
for x being Element of dyadic 0 holds S1[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 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 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;
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 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