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 <> {}

A8: ( 0 in dyadic (n + 1) & 1 in dyadic (n + 1) ) by Th6;

defpred S_{1}[ 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_{1}[x,y]

A12: for x being Element of S holds S_{1}[x,D . x]
from FUNCT_2:sch 3(A9);

defpred S_{2}[ 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_{2}[x,y]

A17: for x being Element of dyadic (n + 1) holds S_{2}[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 )

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 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

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

proof

consider D being Function of S,(bool the carrier of T) such that
let x be Element of S; :: thesis: ex y being Subset of T st S_{1}[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: S_{1}[x, the Between of G . q1,G . q2]

thus S_{1}[x, the Between of G . q1,G . q2]
by A11; :: thesis: verum

end;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: S

thus S

A12: for x being Element of S holds S

defpred S

( ( 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

proof

consider F being Function of (dyadic (n + 1)),(bool the carrier of T) such that
let x be Element of dyadic (n + 1); :: thesis: ex y being Subset of T st S_{2}[x,y]

end;per cases
( x in dyadic n or not x in dyadic n )
;

end;

suppose
x in dyadic n
; :: thesis: ex y being Subset of T st S_{2}[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: S_{2}[x,y]

thus S_{2}[x,y]
by A14; :: thesis: verum

end;consider y being Subset of T such that

A14: y = G . x ;

take y ; :: thesis: S

thus S

suppose A15:
not x in dyadic n
; :: thesis: ex y being Subset of T st S_{2}[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: S_{2}[x,y]

thus S_{2}[x,y]
by A15, A16; :: thesis: verum

end;consider y being Subset of T such that

A16: y = D . x ;

take y ; :: thesis: S

thus S

A17: for x being Element of dyadic (n + 1) holds S

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

end;

thus
( r in dyadic n implies F . r = G . r )
by A17; :: thesis: verumnow :: thesis: ( F . r1 is open & F . r2 is open & Cl (F . r1) c= F . r2 )end;

hence
( F . r1 is open & F . r2 is open & Cl (F . r1) c= F . r2 )
; :: thesis: verumper 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 ) )
;

end;

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;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

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;

end;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 )end;

hence
( F . r1 is open & F . r2 is open & Cl (F . r1) c= F . r2 )
; :: thesis: verumper cases
( r1 = q1 or r1 < q1 )
by A24, XXREAL_0:1;

end;

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;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

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;

end;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 )end;

hence
( F . r1 is open & F . r2 is open & Cl (F . r1) c= F . r2 )
; :: thesis: verumper cases
( q2 = r2 or q2 < r2 )
by A41, XXREAL_0:1;

end;

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;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

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;

end;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 . r2end;

hence
Cl (F . r1) c= F . r2
; :: thesis: verumper cases
( q21 = q12 or q21 < q12 )
by A72, XXREAL_0:1;

end;

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;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

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;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