let T be non empty normal TopSpace; 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; ( 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
; 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]
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;
( 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
;
( 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;
verum
end;
take
F
; ( 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; verum