let T be non empty TopSpace; :: thesis: ( T is normal implies for A, B being closed Subset of T st A <> {} holds
for n being Nat
for G being Function of (dyadic n),(bool the carrier of T) st A c= G . 0 & B = ([#] T) \ (G . 1) & ( 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 ) ) holds
ex F being Function of (dyadic (n + 1)),(bool the carrier of T) st
( A c= F . 0 & B = ([#] T) \ (F . 1) & ( for r1, r2, r being Element of dyadic (n + 1) st r1 < r2 holds
( F . r1 is open & F . r2 is open & Cl (F . r1) c= F . r2 & ( r in dyadic n implies F . r = G . r ) ) ) ) )
assume A1: T is normal ; :: thesis: for A, B being closed Subset of T st A <> {} holds
for n being Nat
for G being Function of (dyadic n),(bool the carrier of T) st A c= G . 0 & B = ([#] T) \ (G . 1) & ( 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 ) ) holds
ex F being Function of (dyadic (n + 1)),(bool the carrier of T) st
( A c= F . 0 & B = ([#] T) \ (F . 1) & ( for r1, r2, r being Element of dyadic (n + 1) st r1 < r2 holds
( F . r1 is open & F . r2 is open & Cl (F . r1) c= F . r2 & ( r in dyadic n implies F . r = G . r ) ) ) )
let A, B be closed Subset of T; :: thesis: ( A <> {} implies for n being Nat
for G being Function of (dyadic n),(bool the carrier of T) st A c= G . 0 & B = ([#] T) \ (G . 1) & ( 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 ) ) holds
ex F being Function of (dyadic (n + 1)),(bool the carrier of T) st
( A c= F . 0 & B = ([#] T) \ (F . 1) & ( for r1, r2, r being Element of dyadic (n + 1) st r1 < r2 holds
( F . r1 is open & F . r2 is open & Cl (F . r1) c= F . r2 & ( r in dyadic n implies F . r = G . r ) ) ) ) )
assume A2: A <> {} ; :: thesis: for n being Nat
for G being Function of (dyadic n),(bool the carrier of T) st A c= G . 0 & B = ([#] T) \ (G . 1) & ( 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 ) ) holds
ex F being Function of (dyadic (n + 1)),(bool the carrier of T) st
( A c= F . 0 & B = ([#] T) \ (F . 1) & ( for r1, r2, r being Element of dyadic (n + 1) st r1 < r2 holds
( F . r1 is open & F . r2 is open & Cl (F . r1) c= F . r2 & ( r in dyadic n implies F . r = G . r ) ) ) )
let n be Nat; :: thesis: for G being Function of (dyadic n),(bool the carrier of T) st A c= G . 0 & B = ([#] T) \ (G . 1) & ( 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 ) ) holds
ex F being Function of (dyadic (n + 1)),(bool the carrier of T) st
( A c= F . 0 & B = ([#] T) \ (F . 1) & ( for r1, r2, r being Element of dyadic (n + 1) st r1 < r2 holds
( F . r1 is open & F . r2 is open & Cl (F . r1) c= F . r2 & ( r in dyadic n implies F . r = G . r ) ) ) )
let G be Function of (dyadic n),(bool the carrier of T); :: thesis: ( A c= G . 0 & B = ([#] T) \ (G . 1) & ( 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 ) ) implies ex F being Function of (dyadic (n + 1)),(bool the carrier of T) st
( A c= F . 0 & B = ([#] T) \ (F . 1) & ( for r1, r2, r being Element of dyadic (n + 1) st r1 < r2 holds
( F . r1 is open & F . r2 is open & Cl (F . r1) c= F . r2 & ( r in dyadic n implies F . r = G . r ) ) ) ) )
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: ex F being Function of (dyadic (n + 1)),(bool the carrier of T) st
( A c= F . 0 & B = ([#] T) \ (F . 1) & ( for r1, r2, r being Element of dyadic (n + 1) st r1 < r2 holds
( F . r1 is open & F . r2 is open & Cl (F . r1) c= F . r2 & ( r in dyadic n implies F . r = G . r ) ) ) )
A6: for r being Element of dyadic n holds G . r <> {}
proof
let r be Element of dyadic n; :: thesis: G . r <> {}
per cases ( 0 = r or 0 < r ) by Th1;
suppose 0 = r ; :: thesis: G . r <> {}
hence G . r <> {} by A2, A3; :: thesis: verum
end;
suppose A7: 0 < r ; :: thesis: G . r <> {}
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: verum
end;
end;
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 S1[ 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 S1[x,y]
proof
let x be Element of S; :: thesis: ex y being Subset of T st S1[x,y]
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: S1[x, the Between of G . q1,G . q2]
thus S1[x, the Between of G . q1,G . q2] by A11; :: thesis: verum
end;
consider D being Function of S,(bool the carrier of T) such that
A12: for x being Element of S holds S1[x,D . x] from FUNCT_2:sch 3(A9);
 defpred S2[ 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 S2[x,y]
proof
let x be Element of dyadic (n + 1); :: thesis: ex y being Subset of T st S2[x,y]
per cases ( x in dyadic n or not x in dyadic n ) ;
suppose x in dyadic n ; :: thesis: ex y being Subset of T st S2[x,y]
then reconsider x = x as Element of dyadic n ;
consider y being Subset of T such that
A14: y = G . x ;
take y ; :: thesis: S2[x,y]
thus S2[x,y] by A14; :: thesis: verum
end;
suppose A15: not x in dyadic n ; :: thesis: ex y being Subset of T st S2[x,y]
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: S2[x,y]
thus S2[x,y] by A15, A16; :: thesis: verum
end;
end;
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 S2[x,F . x] from FUNCT_2:sch 3(A13);
 take F ; :: thesis: ( A c= F . 0 & B = ([#] T) \ (F . 1) & ( for r1, r2, r being Element of dyadic (n + 1) st r1 < r2 holds
( F . r1 is open & F . r2 is open & Cl (F . r1) c= F . r2 & ( r in dyadic n implies F . r = G . r ) ) ) )
( 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: for r1, r2, r being Element of dyadic (n + 1) st r1 < r2 holds
( F . r1 is open & F . r2 is open & Cl (F . r1) c= F . r2 & ( r in dyadic n implies F . r = G . r ) )
let r1, r2, r be Element of dyadic (n + 1); :: thesis: ( r1 < r2 implies ( F . r1 is open & F . r2 is open & Cl (F . r1) c= F . r2 & ( r in dyadic n implies F . r = G . r ) ) )
assume A18: r1 < r2 ; :: thesis: ( F . r1 is open & F . r2 is open & Cl (F . r1) c= F . r2 & ( r in dyadic n implies F . r = G . r ) )
thus ( F . r1 is open & F . r2 is open & Cl (F . r1) c= F . r2 ) :: thesis: ( r in dyadic n implies F . r = G . r )
proof
now :: thesis: ( F . r1 is open & F . r2 is open & Cl (F . r1) c= F . r2 )
per cases ( ( r1 in dyadic n & r2 in dyadic n ) or ( r1 in dyadic n & not r2 in dyadic n ) or ( not r1 in dyadic n & r2 in dyadic n ) or ( not r1 in dyadic n & not r2 in dyadic n ) ) ;
suppose A19: ( r1 in dyadic n & r2 in dyadic n ) ; :: thesis: ( F . r1 is open & F . r2 is open & Cl (F . r1) c= F . r2 )
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: verum
end;
suppose A21: ( r1 in dyadic n & not r2 in dyadic n ) ; :: thesis: ( F . r1 is open & F . r2 is open & Cl (F . r1) c= F . r2 )
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: ( F . r1 is open & F . r2 is open & Cl (F . r1) c= F . r2 )
per cases ( r1 = q1 or r1 < q1 ) by A24, XXREAL_0:1;
suppose r1 = q1 ; :: thesis: ( F . r1 is open & F . r2 is open & Cl (F . r1) c= F . r2 )
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: verum
end;
suppose A32: r1 < q1 ; :: thesis: ( F . r1 is open & F . r2 is open & Cl (F . r1) c= F . r2 )
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: verum
end;
end;
end;
hence ( F . r1 is open & F . r2 is open & Cl (F . r1) c= F . r2 ) ; :: thesis: verum
end;
suppose A38: ( not r1 in dyadic n & r2 in dyadic n ) ; :: thesis: ( F . r1 is open & F . r2 is open & Cl (F . r1) c= F . r2 )
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: ( F . r1 is open & F . r2 is open & Cl (F . r1) c= F . r2 )
per cases ( q2 = r2 or q2 < r2 ) by A41, XXREAL_0:1;
suppose q2 = r2 ; :: thesis: ( F . r1 is open & F . r2 is open & Cl (F . r1) c= F . r2 )
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: verum
end;
suppose A49: q2 < r2 ; :: thesis: ( F . r1 is open & F . r2 is open & Cl (F . r1) c= F . r2 )
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: verum
end;
end;
end;
hence ( F . r1 is open & F . r2 is open & Cl (F . r1) c= F . r2 ) ; :: thesis: verum
end;
suppose A55: ( not r1 in dyadic n & not r2 in dyadic n ) ; :: thesis: ( F . r1 is open & F . r2 is open & Cl (F . r1) c= F . r2 )
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: Cl (F . r1) c= F . r2
A72: q21 <= q12 by A18, A55, A57, A61, Th16;
now :: thesis: Cl (F . r1) c= F . r2
per cases ( q21 = q12 or q21 < q12 ) by A72, XXREAL_0:1;
suppose A73: q21 = q12 ; :: thesis: Cl (F . r1) c= F . r2
( 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: verum
end;
suppose A75: q21 < q12 ; :: thesis: Cl (F . r1) c= F . r2
( 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: verum
end;
end;
end;
hence Cl (F . r1) c= F . r2 ; :: thesis: verum
end;
end;
end;
hence ( F . r1 is open & F . r2 is open & Cl (F . r1) c= F . r2 ) ; :: thesis: verum
end;
thus ( r in dyadic n implies F . r = G . r ) by A17; :: thesis: verum