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 <> {} & A /\ B = {} ) ; :: according to XBOOLE_0:def 7 :: thesis:
let n be Element of NAT ; :: thesis:
let G be Function of dyadic n, bool the carrier of T; :: thesis:
assume that
A3: ( A c= G . 0 & B = ([#] T) \ (G . 1) ) and
A4: 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:
A5: ex x being set st x in A by A2, XBOOLE_0:def 1;
A6: ( 0 in dyadic n & 1 in dyadic n ) by Th12;
A7: for r being Element of dyadic n holds G . r <> {}

proof

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

per cases by Th5;

suppose 0 = r ; :: thesis:

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

end;

suppose A8: 0 < r ; :: thesis:

reconsider q1 = 0 as Element of dyadic n by Th12;
( A c= G . q1 & G . q1 c= Cl (G . q1) & Cl (G . q1) c= G . r ) by A3, A4, A8, PRE_TOPC:48;
then ( A c= Cl (G . q1) & Cl (G . q1) c= G . r ) by XBOOLE_1:1;
then A c= G . r by XBOOLE_1:1;
hence G . r <> {} by A5; :: thesis:

end;

reconsider S = (dyadic (n + 1)) \ (dyadic n) as non empty set by Th15;
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,(n + 1)) - 1) / (2 |^ (n + 1)) & r2 = ((axis r,(n + 1)) + 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: ( x in dyadic (n + 1) & 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,(n + 1)) - 1) / (2 |^ (n + 1)) in dyadic n & ((axis x,(n + 1)) + 1) / (2 |^ (n + 1)) in dyadic n ) by A10, Th20;
then consider q1, q2 being Element of dyadic n such that
A11: q1 = ((axis x,(n + 1)) - 1) / (2 |^ (n + 1)) and
A12: q2 = ((axis x,(n + 1)) + 1) / (2 |^ (n + 1)) ;
consider Q0 being Between of G . q1,G . q2;
take Q0 ; :: thesis:
thus S₁[x,Q0] by A11, A12; :: thesis:

end;

consider D being Function of S, bool the carrier of T such that
A13: 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 ) );
A14: 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
A15: y = G . x ;
take y ; :: thesis:
thus S₂[x,y] by A15; :: thesis:

end;

suppose A16: 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
A17: y = D . x ;
take y ; :: thesis:
thus S₂[x,y] by A16, A17; :: thesis:

end;

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

proof

now

per cases ;

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

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

end;

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

then A23: r2 in S by XBOOLE_0:def 5;
A24: F . r2 = D . r2 by A18, A22;
( ((axis r2,(n + 1)) - 1) / (2 |^ (n + 1)) in dyadic n & ((axis r2,(n + 1)) + 1) / (2 |^ (n + 1)) in dyadic n ) by A22, Th20;
then consider q1, q2 being Element of dyadic n such that
A25: ( q1 = ((axis r2,(n + 1)) - 1) / (2 |^ (n + 1)) & q2 = ((axis r2,(n + 1)) + 1) / (2 |^ (n + 1)) ) ;
D . r2 is Between of G . q1,G . q2 by A13, A23, A25;
then consider D0 being Between of G . q1,G . q2 such that
A26: D0 = D . r2 ;
q1 < q2 by A25, Th18;
then A27: ( G . q1 <> {} & G . q1 is open & G . q2 is open & Cl (G . q1) c= G . q2 ) by A4, A7;
then A28: ( F . r2 <> {} & F . r2 is open & Cl (G . q1) c= F . r2 & Cl (F . r2) c= G . q2 ) by A1, A24, A26, Def10;
A29: r1 <= q1 by A19, A25, Th22;

now

per cases by A29, XXREAL_0:1;

suppose r1 = q1 ; :: thesis:

hence ( F . r1 is open & F . r2 is open & Cl (F . r1) c= F . r2 ) by A18, A27, A28; :: thesis:

end;

suppose A30: r1 < q1 ; :: thesis:

consider q0 being Element of dyadic n such that
A31: q0 = r1 by A22;
( G . q0 is open & G . q1 is open & Cl (G . q0) c= G . q1 & A c= G . 0 & B = ([#] T) \ (G . 1) ) by A3, A4, A30, A31;
then ( F . r1 is open & F . r2 is open & Cl (F . r1) c= G . q1 & G . q1 c= Cl (G . q1) & Cl (G . q1) c= F . r2 ) by A1, A18, A24, A26, A27, A31, Def10, PRE_TOPC:48;
then ( F . r1 is open & F . r2 is open & Cl (F . r1) c= Cl (G . q1) & Cl (G . q1) c= F . r2 ) by XBOOLE_1:1;
hence ( F . r1 is open & F . r2 is open & Cl (F . r1) c= F . r2 ) by XBOOLE_1:1; :: thesis:

end;

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

end;

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

then A33: r1 in S by XBOOLE_0:def 5;
A34: F . r1 = D . r1 by A18, A32;
( ((axis r1,(n + 1)) - 1) / (2 |^ (n + 1)) in dyadic n & ((axis r1,(n + 1)) + 1) / (2 |^ (n + 1)) in dyadic n ) by A32, Th20;
then consider q1, q2 being Element of dyadic n such that
A35: ( q1 = ((axis r1,(n + 1)) - 1) / (2 |^ (n + 1)) & q2 = ((axis r1,(n + 1)) + 1) / (2 |^ (n + 1)) ) ;
D . r1 is Between of G . q1,G . q2 by A13, A33, A35;
then consider D0 being Between of G . q1,G . q2 such that
A36: D0 = D . r1 ;
q1 < q2 by A35, Th18;
then A37: ( G . q1 <> {} & G . q1 is open & G . q2 is open & Cl (G . q1) c= G . q2 ) by A4, A7;
then A38: ( F . r1 <> {} & F . r1 is open & Cl (G . q1) c= F . r1 & Cl (F . r1) c= G . q2 ) by A1, A34, A36, Def10;
A39: q2 <= r2 by A19, A35, Th22;

now

per cases by A39, XXREAL_0:1;

suppose q2 = r2 ; :: thesis:

hence ( F . r1 is open & F . r2 is open & Cl (F . r1) c= F . r2 ) by A18, A37, A38; :: thesis:

end;

suppose A40: q2 < r2 ; :: thesis:

consider q3 being Element of dyadic n such that
A41: q3 = r2 by A32;
( G . q2 is open & G . q3 is open & Cl (G . q2) c= G . q3 & A c= G . 0 & B = ([#] T) \ (G . 1) ) by A3, A4, A40, A41;
then ( F . r1 is open & F . r2 is open & Cl (F . r1) c= G . q2 & G . q2 c= Cl (G . q2) & Cl (G . q2) c= F . r2 ) by A1, A18, A34, A36, A37, A41, Def10, PRE_TOPC:48;
then ( F . r1 is open & F . r2 is open & Cl (F . r1) c= Cl (G . q2) & Cl (G . q2) c= F . r2 ) by XBOOLE_1:1;
hence ( F . r1 is open & F . r2 is open & Cl (F . r1) c= F . r2 ) by XBOOLE_1:1; :: thesis:

end;

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

end;

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

then A43: r1 in S by XBOOLE_0:def 5;
A44: F . r1 = D . r1 by A18, A42;
( ((axis r1,(n + 1)) - 1) / (2 |^ (n + 1)) in dyadic n & ((axis r1,(n + 1)) + 1) / (2 |^ (n + 1)) in dyadic n ) by A42, Th20;
then consider q11, q21 being Element of dyadic n such that
A45: ( q11 = ((axis r1,(n + 1)) - 1) / (2 |^ (n + 1)) & q21 = ((axis r1,(n + 1)) + 1) / (2 |^ (n + 1)) ) ;
D . r1 is Between of G . q11,G . q21 by A13, A43, A45;
then consider D01 being Between of G . q11,G . q21 such that
A46: D01 = D . r1 ;
q11 < q21 by A45, Th18;
then A47: ( G . q11 <> {} & G . q11 is open & G . q21 is open & Cl (G . q11) c= G . q21 ) by A4, A7;
A48: r2 in S by A42, XBOOLE_0:def 5;
A49: F . r2 = D . r2 by A18, A42;
( ((axis r2,(n + 1)) - 1) / (2 |^ (n + 1)) in dyadic n & ((axis r2,(n + 1)) + 1) / (2 |^ (n + 1)) in dyadic n ) by A42, Th20;
then consider q12, q22 being Element of dyadic n such that
A50: ( q12 = ((axis r2,(n + 1)) - 1) / (2 |^ (n + 1)) & q22 = ((axis r2,(n + 1)) + 1) / (2 |^ (n + 1)) ) ;
D . r2 is Between of G . q12,G . q22 by A13, A48, A50;
then consider D02 being Between of G . q12,G . q22 such that
A51: D02 = D . r2 ;
q12 < q22 by A50, Th18;
then A52: ( G . q12 <> {} & G . q12 is open & G . q22 is open & Cl (G . q12) c= G . q22 ) by A4, A7;
hence ( F . r1 is open & F . r2 is open ) by A1, A44, A46, A47, A49, A51, Def10; :: thesis:
A53: q21 <= q12 by A19, A42, A45, A50, Th23;

now

per cases by A53, XXREAL_0:1;

suppose q21 = q12 ; :: thesis:

then ( Cl (F . r1) c= G . q21 & G . q21 c= Cl (G . q21) & Cl (G . q21) c= F . r2 ) by A1, A44, A46, A47, A49, A51, A52, Def10, PRE_TOPC:48;
then ( Cl (F . r1) c= Cl (G . q21) & Cl (G . q21) c= F . r2 ) by XBOOLE_1:1;
hence Cl (F . r1) c= F . r2 by XBOOLE_1:1; :: thesis:

end;

suppose q21 < q12 ; :: thesis:

then ( Cl (F . r1) c= G . q21 & G . q21 c= Cl (G . q21) & G . q12 c= Cl (G . q12) & Cl (G . q21) c= G . q12 & Cl (G . q12) c= F . r2 ) by A1, A4, A44, A46, A47, A49, A51, A52, Def10, PRE_TOPC:48;
then ( Cl (F . r1) c= Cl (G . q21) & Cl (G . q21) c= G . q12 & G . q12 c= F . r2 ) by XBOOLE_1:1;
then ( Cl (F . r1) c= G . q12 & G . q12 c= F . r2 ) by XBOOLE_1:1;
hence Cl (F . r1) c= F . r2 by XBOOLE_1:1; :: 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 A18; :: thesis: