let T be non empty TopSpace; :: thesis:
assume A1: T is normal ; :: thesis:
let A, B be closed Subset of T; :: thesis:
assume A2: A <> {} ; :: thesis:
let n be Nat; :: thesis:
let G be Function of (dyadic n),(bool the carrier of T); :: thesis:
assume that
A3: A c= G . 0 and
A4: B = ([#] T) \ (G . 1) and
A5: for r1, r2 being Element of dyadic n st r1 < r2 holds
( G . r1 is open & G . r2 is open & Cl (G . r1) c= G . r2 ) ; :: thesis:
A6: for r being Element of dyadic n holds G . r <> {}

let r be Element of dyadic n; :: thesis:

per cases by Th1;

suppose 0 = r ; :: thesis:

hence G . r <> {} by A2, A3; :: thesis:

end;

suppose A7: 0 < r ; :: thesis:

reconsider q1 = 0 as Element of dyadic n by Th6;
( G . q1 c= Cl (G . q1) & Cl (G . q1) c= G . r ) by A5, A7, PRE_TOPC:18;
hence G . r <> {} by A2, A3; :: thesis:

end;

reconsider S = (dyadic (n + 1)) \ (dyadic n) as non empty set by Th9;
A8: ( 0 in dyadic (n + 1) & 1 in dyadic (n + 1) ) by Th6;
defpred S₁[ Element of S, Subset of T] means for r being Element of dyadic (n + 1) st r in S & $1 = r holds
for r1, r2 being Element of dyadic n st r1 = ((axis r) - 1) / (2 |^ (n + 1)) & r2 = ((axis r) + 1) / (2 |^ (n + 1)) holds
$2 is Between of G . r1,G . r2;
A9: for x being Element of S ex y being Subset of T st S₁[x,y]

proof

let x be Element of S; :: thesis:
A10: not x in dyadic n by XBOOLE_0:def 5;
reconsider x = x as Element of dyadic (n + 1) by XBOOLE_0:def 5;
( ((axis x) - 1) / (2 |^ (n + 1)) in dyadic n & ((axis x) + 1) / (2 |^ (n + 1)) in dyadic n ) by A10, Th13;
then consider q1, q2 being Element of dyadic n such that
A11: ( q1 = ((axis x) - 1) / (2 |^ (n + 1)) & q2 = ((axis x) + 1) / (2 |^ (n + 1)) ) ;
take the Between of G . q1,G . q2 ; :: thesis:
thus S₁[x, the Between of G . q1,G . q2] by A11; :: thesis:

end;

consider D being Function of S,(bool the carrier of T) such that
A12: for x being Element of S holds S₁[x,D . x] from FUNCT_2:sch 3(A9);
defpred S₂[ Element of dyadic (n + 1), Subset of T] means for r being Element of dyadic (n + 1) st $1 = r holds
( ( r in dyadic n implies $2 = G . r ) & ( not r in dyadic n implies $2 = D . r ) );
A13: for x being Element of dyadic (n + 1) ex y being Subset of T st S₂[x,y]

proof

let x be Element of dyadic (n + 1); :: thesis:

per cases ;

suppose x in dyadic n ; :: thesis:

then reconsider x = x as Element of dyadic n ;
consider y being Subset of T such that
A14: y = G . x ;
take y ; :: thesis:
thus S₂[x,y] by A14; :: thesis:

end;

suppose A15: not x in dyadic n ; :: thesis:

then reconsider x = x as Element of S by XBOOLE_0:def 5;
consider y being Subset of T such that
A16: y = D . x ;
take y ; :: thesis:
thus S₂[x,y] by A15, A16; :: thesis:

end;

consider F being Function of (dyadic (n + 1)),(bool the carrier of T) such that
A17: for x being Element of dyadic (n + 1) holds S₂[x,F . x] from FUNCT_2:sch 3(A13);
take F ; :: thesis:
( 0 in dyadic n & 1 in dyadic n ) by Th6;
hence ( A c= F . 0 & B = ([#] T) \ (F . 1) ) by A3, A4, A17, A8; :: thesis:
let r1, r2, r be Element of dyadic (n + 1); :: thesis:
assume A18: r1 < r2 ; :: thesis:
thus ( F . r1 is open & F . r2 is open & Cl (F . r1) c= F . r2 ) :: thesis:

proof

now :: thesis:

per cases ;

suppose A19: ( r1 in dyadic n & r2 in dyadic n ) ; :: thesis:

then A20: ( F . r1 = G . r1 & F . r2 = G . r2 ) by A17;
reconsider r1 = r1, r2 = r2 as Element of dyadic n by A19;
r1 < r2 by A18;
hence ( F . r1 is open & F . r2 is open & Cl (F . r1) c= F . r2 ) by A5, A20; :: thesis:

end;

suppose A21: ( r1 in dyadic n & not r2 in dyadic n ) ; :: thesis:

then ( ((axis r2) - 1) / (2 |^ (n + 1)) in dyadic n & ((axis r2) + 1) / (2 |^ (n + 1)) in dyadic n ) by Th13;
then consider q1, q2 being Element of dyadic n such that
A22: q1 = ((axis r2) - 1) / (2 |^ (n + 1)) and
A23: q2 = ((axis r2) + 1) / (2 |^ (n + 1)) ;
A24: r1 <= q1 by A18, A22, Th15;
r2 in S by A21, XBOOLE_0:def 5;
then A25: D . r2 is Between of G . q1,G . q2 by A12, A22, A23;
A26: q1 < q2 by A22, A23, Th12;
then A27: ( G . q2 is open & Cl (G . q1) c= G . q2 ) by A5;
A28: F . r2 = D . r2 by A17, A21;
A29: G . q1 <> {} by A6;
A30: G . q1 is open by A5, A26;
then A31: Cl (G . q1) c= F . r2 by A1, A28, A25, A29, A27, Def8;

now :: thesis:

per cases by A24, XXREAL_0:1;

suppose r1 = q1 ; :: thesis:

hence ( F . r1 is open & F . r2 is open & Cl (F . r1) c= F . r2 ) by A1, A17, A28, A25, A29, A30, A27, A31, Def8; :: thesis:

end;

suppose A32: r1 < q1 ; :: thesis:

A33: G . q1 c= Cl (G . q1) by PRE_TOPC:18;
consider q0 being Element of dyadic n such that
A34: q0 = r1 by A21;
Cl (G . q0) c= G . q1 by A5, A32, A34;
then Cl (F . r1) c= G . q1 by A17, A34;
then A35: Cl (F . r1) c= Cl (G . q1) by A33;
A36: G . q0 is open by A5, A32, A34;
A37: G . q1 is open by A5, A32, A34;
then Cl (G . q1) c= F . r2 by A1, A28, A25, A29, A27, Def8;
hence ( F . r1 is open & F . r2 is open & Cl (F . r1) c= F . r2 ) by A1, A17, A28, A25, A29, A27, A34, A36, A37, A35, Def8; :: thesis:

end;

hence ( F . r1 is open & F . r2 is open & Cl (F . r1) c= F . r2 ) ; :: thesis:

end;

suppose A38: ( not r1 in dyadic n & r2 in dyadic n ) ; :: thesis:

then ( ((axis r1) - 1) / (2 |^ (n + 1)) in dyadic n & ((axis r1) + 1) / (2 |^ (n + 1)) in dyadic n ) by Th13;
then consider q1, q2 being Element of dyadic n such that
A39: q1 = ((axis r1) - 1) / (2 |^ (n + 1)) and
A40: q2 = ((axis r1) + 1) / (2 |^ (n + 1)) ;
A41: q2 <= r2 by A18, A40, Th15;
r1 in S by A38, XBOOLE_0:def 5;
then A42: D . r1 is Between of G . q1,G . q2 by A12, A39, A40;
A43: q1 < q2 by A39, A40, Th12;
then A44: ( G . q1 is open & Cl (G . q1) c= G . q2 ) by A5;
A45: F . r1 = D . r1 by A17, A38;
A46: G . q1 <> {} by A6;
A47: G . q2 is open by A5, A43;
then A48: Cl (F . r1) c= G . q2 by A1, A45, A42, A46, A44, Def8;

now :: thesis:

per cases by A41, XXREAL_0:1;

suppose q2 = r2 ; :: thesis:

hence ( F . r1 is open & F . r2 is open & Cl (F . r1) c= F . r2 ) by A1, A17, A45, A42, A46, A47, A44, A48, Def8; :: thesis:

end;

suppose A49: q2 < r2 ; :: thesis:

A50: G . q2 c= Cl (G . q2) by PRE_TOPC:18;
consider q3 being Element of dyadic n such that
A51: q3 = r2 by A38;
A52: G . q2 is open by A5, A49, A51;
then Cl (F . r1) c= G . q2 by A1, A45, A42, A46, A44, Def8;
then A53: Cl (F . r1) c= Cl (G . q2) by A50;
Cl (G . q2) c= G . q3 by A5, A49, A51;
then A54: Cl (G . q2) c= F . r2 by A17, A51;
G . q3 is open by A5, A49, A51;
hence ( F . r1 is open & F . r2 is open & Cl (F . r1) c= F . r2 ) by A1, A17, A45, A42, A46, A44, A51, A52, A53, A54, Def8; :: thesis:

end;

hence ( F . r1 is open & F . r2 is open & Cl (F . r1) c= F . r2 ) ; :: thesis:

end;

suppose A55: ( not r1 in dyadic n & not r2 in dyadic n ) ; :: thesis:

then ( ((axis r1) - 1) / (2 |^ (n + 1)) in dyadic n & ((axis r1) + 1) / (2 |^ (n + 1)) in dyadic n ) by Th13;
then consider q11, q21 being Element of dyadic n such that
A56: q11 = ((axis r1) - 1) / (2 |^ (n + 1)) and
A57: q21 = ((axis r1) + 1) / (2 |^ (n + 1)) ;
r1 in S by A55, XBOOLE_0:def 5;
then A58: D . r1 is Between of G . q11,G . q21 by A12, A56, A57;
A59: q11 < q21 by A56, A57, Th12;
then A60: G . q21 is open by A5;
( ((axis r2) - 1) / (2 |^ (n + 1)) in dyadic n & ((axis r2) + 1) / (2 |^ (n + 1)) in dyadic n ) by A55, Th13;
then consider q12, q22 being Element of dyadic n such that
A61: q12 = ((axis r2) - 1) / (2 |^ (n + 1)) and
A62: q22 = ((axis r2) + 1) / (2 |^ (n + 1)) ;
r2 in S by A55, XBOOLE_0:def 5;
then A63: D . r2 is Between of G . q12,G . q22 by A12, A61, A62;
A64: q12 < q22 by A61, A62, Th12;
then A65: G . q12 is open by A5;
A66: ( G . q22 is open & Cl (G . q12) c= G . q22 ) by A5, A64;
A67: G . q12 <> {} by A6;
A68: G . q11 <> {} by A6;
A69: F . r2 = D . r2 by A17, A55;
A70: F . r1 = D . r1 by A17, A55;
A71: ( G . q11 is open & Cl (G . q11) c= G . q21 ) by A5, A59;
hence ( F . r1 is open & F . r2 is open ) by A1, A70, A58, A68, A60, A69, A63, A67, A65, A66, Def8; :: thesis:
A72: q21 <= q12 by A18, A55, A57, A61, Th16;

now :: thesis:

per cases by A72, XXREAL_0:1;

suppose A73: q21 = q12 ; :: thesis:

( Cl (F . r1) c= G . q21 & G . q21 c= Cl (G . q21) ) by A1, A70, A58, A68, A60, A71, Def8, PRE_TOPC:18;
then A74: Cl (F . r1) c= Cl (G . q21) ;
Cl (G . q21) c= F . r2 by A1, A60, A69, A63, A67, A66, A73, Def8;
hence Cl (F . r1) c= F . r2 by A74; :: thesis:

end;

suppose A75: q21 < q12 ; :: thesis:

( Cl (F . r1) c= G . q21 & G . q21 c= Cl (G . q21) ) by A1, A70, A58, A68, A60, A71, Def8, PRE_TOPC:18;
then A76: Cl (F . r1) c= Cl (G . q21) ;
Cl (G . q21) c= G . q12 by A5, A75;
then A77: Cl (F . r1) c= G . q12 by A76;
( G . q12 c= Cl (G . q12) & Cl (G . q12) c= F . r2 ) by A1, A69, A63, A67, A65, A66, Def8, PRE_TOPC:18;
then G . q12 c= F . r2 ;
hence Cl (F . r1) c= F . r2 by A77; :: thesis:

end;

hence Cl (F . r1) c= F . r2 ; :: thesis:

end;

hence ( F . r1 is open & F . r2 is open & Cl (F . r1) c= F . r2 ) ; :: thesis:

end;

thus ( r in dyadic n implies F . r = G . r ) by A17; :: thesis: