:: URYSOHN3 semantic presentation

begin

Lm1:  for T being 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 ) ) )
proof
let T be non empty normal TopSpace; ::_thesis: 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; ::_thesis: ( 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 ; ::_thesis: 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]
proof
let x be Element of dyadic 0; ::_thesis: ex y being Subset of T st S1[x,y]
percases ( x = 0 or x = 1 ) by TARSKI:def_2, URYSOHN1:2;
supposeA9: x = 0 ; ::_thesis: ex y being Subset of T st S1[x,y]
take  G0 ; ::_thesis: S1[x,G0]
thus  S1[x,G0] by A9; ::_thesis: verum
end;
supposeA10: x = 1 ; ::_thesis: ex y being Subset of T st S1[x,y]
take  G1 ; ::_thesis: S1[x,G1]
thus  S1[x,G1] by A10; ::_thesis: verum
end;
end;
end;
 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; ::_thesis: ( 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 ; ::_thesis: ( 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; ::_thesis: verum
end;
take  F ; ::_thesis: ( 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; ::_thesis: verum
end;

theorem Th1: :: URYSOHN3:1
for T being non empty normal TopSpace
for A, B being closed Subset of T st A <> {} & A misses B holds
for n being Element of NAT ex 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 ) ) )
proof
let T be non empty normal TopSpace; ::_thesis: for A, B being closed Subset of T st A <> {} & A misses B holds
for n being Element of NAT ex 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 ) ) )
let A, B be closed Subset of T; ::_thesis: ( A <> {} & A misses B implies for n being Element of NAT ex 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 ) ) ) )
assume that
A1: A <> {} and
A2: A misses B ; ::_thesis: for n being Element of NAT ex 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 ) ) )
defpred S1[ Element of NAT ] means  ex G being Function of (dyadic $1),(bool the carrier of T) st
( A c= G . 0 & B = ([#] T) \ (G . 1) & ( for r1, r2 being Element of dyadic $1 st r1 < r2 holds
( G . r1 is open & G . r2 is open & Cl (G . r1) c= G . r2 ) ) );
A3: for n being Element of NAT st S1[n] holds
S1[n + 1]
proof
let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] )
given G being Function of (dyadic n),(bool the carrier of T) such that A4: ( 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 ) ) ) ; ::_thesis: S1[n + 1]
consider F being Function of (dyadic (n + 1)),(bool the carrier of T) such that
A5: ( 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 ) ) ) ) by A1, A4, URYSOHN1:24;
take  F ; ::_thesis: ( A c= F . 0 & B = ([#] T) \ (F . 1) & ( for r1, r2 being Element of dyadic (n + 1) st r1 < r2 holds
( F . r1 is open & F . r2 is open & Cl (F . r1) c= F . r2 ) ) )
thus  ( A c= F . 0 & B = ([#] T) \ (F . 1) & ( for r1, r2 being Element of dyadic (n + 1) st r1 < r2 holds
( F . r1 is open & F . r2 is open & Cl (F . r1) c= F . r2 ) ) ) by A5; ::_thesis: verum
end;
A6: S1[ 0 ] by A1, A2, Lm1;
thus  for n being Element of NAT holds S1[n] from NAT_1:sch_1(A6, A3); ::_thesis: verum
end;

definition
let T be non empty TopSpace;
let A, B be Subset of T;
let n be Element of NAT ;
assume A1: ( T is normal & A <> {} & A is closed & B is closed & A misses B ) ;
mode Drizzle of A,B,n ->  Function of (dyadic n),(bool the carrier of T) means :Def1: :: URYSOHN3:def 1
( A c= it . 0 & B = ([#] T) \ (it . 1) & ( for r1, r2 being Element of dyadic n st r1 < r2 holds
( it . r1 is open & it . r2 is open & Cl (it . r1) c= it . r2 ) ) );
existence
 ex b1 being Function of (dyadic n),(bool the carrier of T) st
( A c= b1 . 0 & B = ([#] T) \ (b1 . 1) & ( for r1, r2 being Element of dyadic n st r1 < r2 holds
( b1 . r1 is open & b1 . r2 is open & Cl (b1 . r1) c= b1 . r2 ) ) ) by A1, Th1;
end;

:: deftheorem Def1 defines Drizzle URYSOHN3:def_1_:_
 for T being non empty TopSpace
for A, B being Subset of T
for n being Element of NAT st T is normal & A <> {} & A is closed & B is closed & A misses B holds
for b5 being Function of (dyadic n),(bool the carrier of T) holds
( b5 is Drizzle of A,B,n iff ( A c= b5 . 0 & B = ([#] T) \ (b5 . 1) & ( for r1, r2 being Element of dyadic n st r1 < r2 holds
( b5 . r1 is open & b5 . r2 is open & Cl (b5 . r1) c= b5 . r2 ) ) ) );

theorem Th2: :: URYSOHN3:2
for T being non empty normal TopSpace
for A, B being closed Subset of T st A <> {} & A misses B holds
for n being Element of NAT
for G being Drizzle of A,B,n ex F being Drizzle of A,B,n + 1 st
for r being Element of dyadic (n + 1) st r in dyadic n holds
F . r = G . r
proof
let T be non empty normal TopSpace; ::_thesis: for A, B being closed Subset of T st A <> {} & A misses B holds
for n being Element of NAT
for G being Drizzle of A,B,n ex F being Drizzle of A,B,n + 1 st
for r being Element of dyadic (n + 1) st r in dyadic n holds
F . r = G . r
let A, B be closed Subset of T; ::_thesis: ( A <> {} & A misses B implies for n being Element of NAT
for G being Drizzle of A,B,n ex F being Drizzle of A,B,n + 1 st
for r being Element of dyadic (n + 1) st r in dyadic n holds
F . r = G . r )
assume that
A1: A <> {} and
A2: A misses B ; ::_thesis: for n being Element of NAT
for G being Drizzle of A,B,n ex F being Drizzle of A,B,n + 1 st
for r being Element of dyadic (n + 1) st r in dyadic n holds
F . r = G . r
let n be Element of NAT ; ::_thesis: for G being Drizzle of A,B,n ex F being Drizzle of A,B,n + 1 st
for r being Element of dyadic (n + 1) st r in dyadic n holds
F . r = G . r
let G be Drizzle of A,B,n; ::_thesis: ex F being Drizzle of A,B,n + 1 st
for r being Element of dyadic (n + 1) st r in dyadic n holds
F . r = G . r
A3: 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 ) by A1, A2, Def1;
 ( A c= G . 0 & B = ([#] T) \ (G . 1) ) by A1, A2, Def1;
then consider F being Function of (dyadic (n + 1)),(bool the carrier of T) such that
A4: ( A c= F . 0 & B = ([#] T) \ (F . 1) ) and
A5: 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 ) ) by A1, A3, URYSOHN1:24;
 for r1, r2 being Element of dyadic (n + 1) st r1 < r2 holds
( F . r1 is open & F . r2 is open & Cl (F . r1) c= F . r2 ) by A5;
then reconsider F = F as Drizzle of A,B,n + 1 by A1, A2, A4, Def1;
take  F ; ::_thesis: for r being Element of dyadic (n + 1) st r in dyadic n holds
F . r = G . r
let r be Element of dyadic (n + 1); ::_thesis: ( r in dyadic n implies F . r = G . r )
A6: ( 0 in dyadic (n + 1) & 1 in dyadic (n + 1) ) by URYSOHN1:6;
assume  r in dyadic n ; ::_thesis: F . r = G . r
hence  F . r = G . r by A5, A6; ::_thesis: verum
end;

theorem Th3: :: URYSOHN3:3
for T being non empty TopSpace
for A, B being Subset of T
for n being Element of NAT
for S being Drizzle of A,B,n holds S is Element of PFuncs (DYADIC,(bool the carrier of T))
proof
let T be non empty TopSpace; ::_thesis: for A, B being Subset of T
for n being Element of NAT
for S being Drizzle of A,B,n holds S is Element of PFuncs (DYADIC,(bool the carrier of T))
let A, B be Subset of T; ::_thesis: for n being Element of NAT
for S being Drizzle of A,B,n holds S is Element of PFuncs (DYADIC,(bool the carrier of T))
let n be Element of NAT ; ::_thesis: for S being Drizzle of A,B,n holds S is Element of PFuncs (DYADIC,(bool the carrier of T))
let S be Drizzle of A,B,n; ::_thesis: S is Element of PFuncs (DYADIC,(bool the carrier of T))
 dyadic n c= DYADIC by URYSOHN2:23;
then  S is PartFunc of DYADIC,(bool the carrier of T) by RELSET_1:7;
hence  S is Element of PFuncs (DYADIC,(bool the carrier of T)) by PARTFUN1:45; ::_thesis: verum
end;

definition
let A, B be non empty set ;
let F be Function of NAT,(PFuncs (A,B));
let n be Element of NAT ;
:: original: .
redefine funcF . n ->  Element of PFuncs (A,B);
coherence
 F . n is Element of PFuncs (A,B) by FUNCT_2:5;
end;

theorem Th4: :: URYSOHN3:4
for T being non empty normal TopSpace
for A, B being closed Subset of T st A <> {} & A misses B holds
ex F being Functional_Sequence of DYADIC,(bool the carrier of T) st
for n being Element of NAT holds
( F . n is Drizzle of A,B,n & ( for r being Element of dom (F . n) holds (F . n) . r = (F . (n + 1)) . r ) )
proof
let T be non empty normal TopSpace; ::_thesis: for A, B being closed Subset of T st A <> {} & A misses B holds
ex F being Functional_Sequence of DYADIC,(bool the carrier of T) st
for n being Element of NAT holds
( F . n is Drizzle of A,B,n & ( for r being Element of dom (F . n) holds (F . n) . r = (F . (n + 1)) . r ) )
let A, B be closed Subset of T; ::_thesis: ( A <> {} & A misses B implies ex F being Functional_Sequence of DYADIC,(bool the carrier of T) st
for n being Element of NAT holds
( F . n is Drizzle of A,B,n & ( for r being Element of dom (F . n) holds (F . n) . r = (F . (n + 1)) . r ) ) )
defpred S1[ set ] means  ex n being Element of NAT st $1 is Drizzle of A,B,n;
consider D being set  such that
A1: for x being set holds
( x in D iff ( x in PFuncs (DYADIC,(bool the carrier of T)) & S1[x] ) ) from XBOOLE_0:sch_1();
set S = the Drizzle of A,B, 0 ;
A2: the Drizzle of A,B, 0 is Element of PFuncs (DYADIC,(bool the carrier of T)) by Th3;
then reconsider D = D as non empty set by A1;
reconsider S = the Drizzle of A,B, 0 as Element of D by A1, A2;
defpred S2[ Element of D, Element of D] means  ex xx, yy being PartFunc of DYADIC,(bool the carrier of T) st
( xx = $1 & yy = $2 & ex k being Element of NAT st xx is Drizzle of A,B,k & ( for k being Element of NAT st xx is Drizzle of A,B,k holds
yy is Drizzle of A,B,k + 1 ) & ( for r being Element of dom xx holds xx . r = yy . r ) );
defpred S3[ Element of NAT , Element of D, Element of D] means S2[$2,$3];
assume A3: ( A <> {} & A misses B ) ; ::_thesis: ex F being Functional_Sequence of DYADIC,(bool the carrier of T) st
for n being Element of NAT holds
( F . n is Drizzle of A,B,n & ( for r being Element of dom (F . n) holds (F . n) . r = (F . (n + 1)) . r ) )
A4: for n being Element of NAT
for x being Element of D ex y being Element of D st S3[n,x,y]
proof
let n be Element of NAT ; ::_thesis: for x being Element of D ex y being Element of D st S3[n,x,y]
let x be Element of D; ::_thesis: ex y being Element of D st S3[n,x,y]
consider s0 being Element of NAT  such that
A5: x is Drizzle of A,B,s0 by A1;
reconsider xx = x as Drizzle of A,B,s0 by A5;
consider yy being Drizzle of A,B,s0 + 1 such that
A6: for r being Element of dyadic (s0 + 1) st r in dyadic s0 holds
yy . r = xx . r by A3, Th2;
A7: for r being Element of dom xx holds xx . r = yy . r
proof
let r be Element of dom xx; ::_thesis: xx . r = yy . r
 dom xx = dyadic s0 by FUNCT_2:def_1;
then A8: r in dyadic s0 ;
 dyadic s0 c= dyadic (s0 + 1) by URYSOHN1:5;
hence  xx . r = yy . r by A6, A8; ::_thesis: verum
end;
A9: for k being Element of NAT st xx is Drizzle of A,B,k holds
yy is Drizzle of A,B,k + 1
proof
let k be Element of NAT ; ::_thesis: ( xx is Drizzle of A,B,k implies yy is Drizzle of A,B,k + 1 )
assume  xx is Drizzle of A,B,k ; ::_thesis: yy is Drizzle of A,B,k + 1
then A10: dom xx = dyadic k by FUNCT_2:def_1;
 k = s0
proof
assume A11: k <> s0 ; ::_thesis: contradiction
percases ( k < s0 or s0 < k ) by A11, XXREAL_0:1;
supposeA12: k < s0 ; ::_thesis: contradiction
set o = 1 / (2 |^ s0);
A13: not 1 / (2 |^ s0) in dyadic k
proof
A14: 2 |^ k < 1 * (2 |^ s0) by A12, PEPIN:66;
assume  1 / (2 |^ s0) in dyadic k ; ::_thesis: contradiction
then consider i being Element of NAT  such that
 i <= 2 |^ k and
A15: 1 / (2 |^ s0) = i / (2 |^ k) by URYSOHN1:def_1;
A16: 0 < 2 |^ s0 by NEWTON:83;
 0 < 2 |^ k by NEWTON:83;
then A17: 1 * (2 |^ k) = i * (2 |^ s0) by A15, A16, XCMPLX_1:95;
then A18: i = (2 |^ k) / (2 |^ s0) by A16, XCMPLX_1:89;
A19: for n being Nat holds not i = n + 1
proof
given n being Nat such that A20: i = n + 1 ; ::_thesis: contradiction
 (n + 1) - 1 < 0 by A18, A14, A20, XREAL_1:49, XREAL_1:83;
hence  contradiction ; ::_thesis: verum
end;
 i <> 0 by A17, NEWTON:83;
hence  contradiction by A19, NAT_1:6; ::_thesis: verum
end;
 1 <= 2 |^ s0 by PREPOWER:11;
then  1 / (2 |^ s0) in dyadic s0 by URYSOHN1:def_1;
hence  contradiction by A10, A13, FUNCT_2:def_1; ::_thesis: verum
end;
supposeA21: s0 < k ; ::_thesis: contradiction
set o = 1 / (2 |^ k);
A22: not 1 / (2 |^ k) in dyadic s0
proof
A23: 2 |^ s0 < 1 * (2 |^ k) by A21, PEPIN:66;
assume  1 / (2 |^ k) in dyadic s0 ; ::_thesis: contradiction
then consider i being Element of NAT  such that
 i <= 2 |^ s0 and
A24: 1 / (2 |^ k) = i / (2 |^ s0) by URYSOHN1:def_1;
A25: 0 < 2 |^ k by NEWTON:83;
 0 < 2 |^ s0 by NEWTON:83;
then A26: 1 * (2 |^ s0) = i * (2 |^ k) by A24, A25, XCMPLX_1:95;
then A27: i = (2 |^ s0) / (2 |^ k) by A25, XCMPLX_1:89;
A28: for n being Nat holds not i = n + 1
proof
given n being Nat such that A29: i = n + 1 ; ::_thesis: contradiction
 (n + 1) - 1 < 0 by A27, A23, A29, XREAL_1:49, XREAL_1:83;
hence  contradiction ; ::_thesis: verum
end;
 i <> 0 by A26, NEWTON:83;
hence  contradiction by A28, NAT_1:6; ::_thesis: verum
end;
 1 <= 2 |^ k by PREPOWER:11;
then  1 / (2 |^ k) in dyadic k by URYSOHN1:def_1;
hence  contradiction by A10, A22, FUNCT_2:def_1; ::_thesis: verum
end;
end;
end;
hence  yy is Drizzle of A,B,k + 1 ; ::_thesis: verum
end;
reconsider xx = xx as Element of PFuncs (DYADIC,(bool the carrier of T)) by Th3;
reconsider xx = xx as Element of D ;
A30: yy is Element of PFuncs (DYADIC,(bool the carrier of T)) by Th3;
then reconsider yy = yy as Element of D by A1;
 ex y being Element of D st S2[x,y]
proof
take  yy ; ::_thesis: S2[x,yy]
reconsider yy = yy as PartFunc of DYADIC,(bool the carrier of T) by A30, PARTFUN1:46;
reconsider xx = xx as PartFunc of DYADIC,(bool the carrier of T) by PARTFUN1:47;
take  xx ; ::_thesis: ex yy being PartFunc of DYADIC,(bool the carrier of T) st
( xx = x & yy = yy & ex k being Element of NAT st xx is Drizzle of A,B,k & ( for k being Element of NAT st xx is Drizzle of A,B,k holds
yy is Drizzle of A,B,k + 1 ) & ( for r being Element of dom xx holds xx . r = yy . r ) )
take  yy ; ::_thesis: ( xx = x & yy = yy & ex k being Element of NAT st xx is Drizzle of A,B,k & ( for k being Element of NAT st xx is Drizzle of A,B,k holds
yy is Drizzle of A,B,k + 1 ) & ( for r being Element of dom xx holds xx . r = yy . r ) )
thus  ( xx = x & yy = yy & ex k being Element of NAT st xx is Drizzle of A,B,k & ( for k being Element of NAT st xx is Drizzle of A,B,k holds
yy is Drizzle of A,B,k + 1 ) & ( for r being Element of dom xx holds xx . r = yy . r ) ) by A9, A7; ::_thesis: verum
end;
then consider y being Element of D such that
A31: S2[x,y] ;
take  y ; ::_thesis: S3[n,x,y]
thus  S3[n,x,y] by A31; ::_thesis: verum
end;
 ex F being Function of NAT,D st
( F . 0 = S & ( for n being Element of NAT holds S3[n,F . n,F . (n + 1)] ) ) from RECDEF_1:sch_2(A4);
then consider F being Function of NAT,D such that
A32: F . 0 = S and
A33: for n being Element of NAT holds S2[F . n,F . (n + 1)] ;
 for x being set st x in D holds
x in PFuncs (DYADIC,(bool the carrier of T)) by A1;
then  ( rng F c= D & D c= PFuncs (DYADIC,(bool the carrier of T)) ) by RELAT_1:def_19, TARSKI:def_3;
then A34: ( dom F = NAT & rng F c= PFuncs (DYADIC,(bool the carrier of T)) ) by FUNCT_2:def_1, XBOOLE_1:1;
defpred S4[ Element of NAT , PartFunc of DYADIC,(bool the carrier of T), PartFunc of DYADIC,(bool the carrier of T)] means ( $2 = F . $1 & $3 = F . ($1 + 1) & ex k being Element of NAT st $2 is Drizzle of A,B,k & ( for k being Element of NAT st $2 is Drizzle of A,B,k holds
$3 is Drizzle of A,B,k + 1 ) & ( for r being Element of dom $2 holds $2 . r = $3 . r ) );
reconsider F = F as Functional_Sequence of DYADIC,(bool the carrier of T) by A34, FUNCT_2:def_1, RELSET_1:4;
defpred S5[ Element of NAT ] means ( F . $1 is Drizzle of A,B,$1 & ( for r being Element of dom (F . $1) holds (F . $1) . r = (F . ($1 + 1)) . r ) );
A35: for n being Element of NAT st S5[n] holds
S5[n + 1]
proof
let n be Element of NAT ; ::_thesis: ( S5[n] implies S5[n + 1] )
assume A36: S5[n] ; ::_thesis: S5[n + 1]
 ex xx, yy being PartFunc of DYADIC,(bool the carrier of T) st S4[n,xx,yy] by A33;
hence  F . (n + 1) is Drizzle of A,B,n + 1 by A36; ::_thesis: for r being Element of dom (F . (n + 1)) holds (F . (n + 1)) . r = (F . ((n + 1) + 1)) . r
let r be Element of dom (F . (n + 1)); ::_thesis: (F . (n + 1)) . r = (F . ((n + 1) + 1)) . r
 ex xx1, yy1 being PartFunc of DYADIC,(bool the carrier of T) st S4[n + 1,xx1,yy1] by A33;
hence  (F . (n + 1)) . r = (F . ((n + 1) + 1)) . r ; ::_thesis: verum
end;
take  F ; ::_thesis: for n being Element of NAT holds
( F . n is Drizzle of A,B,n & ( for r being Element of dom (F . n) holds (F . n) . r = (F . (n + 1)) . r ) )
 ex xx, yy being PartFunc of DYADIC,(bool the carrier of T) st S4[ 0 ,xx,yy] by A33;
then A37: S5[ 0 ] by A32;
 for n being Element of NAT holds S5[n] from NAT_1:sch_1(A37, A35);
hence  for n being Element of NAT holds
( F . n is Drizzle of A,B,n & ( for r being Element of dom (F . n) holds (F . n) . r = (F . (n + 1)) . r ) ) ; ::_thesis: verum
end;

definition
let T be non empty TopSpace;
let A, B be Subset of T;
assume A1: ( T is normal & A <> {} & A is closed & B is closed & A misses B ) ;
mode Rain of A,B ->  Functional_Sequence of DYADIC,(bool the carrier of T) means :Def2: :: URYSOHN3:def 2
 for n being Element of NAT holds
( it . n is Drizzle of A,B,n & ( for r being Element of dom (it . n) holds (it . n) . r = (it . (n + 1)) . r ) );
existence
 ex b1 being Functional_Sequence of DYADIC,(bool the carrier of T) st
for n being Element of NAT holds
( b1 . n is Drizzle of A,B,n & ( for r being Element of dom (b1 . n) holds (b1 . n) . r = (b1 . (n + 1)) . r ) ) by A1, Th4;
end;

:: deftheorem Def2 defines Rain URYSOHN3:def_2_:_
 for T being non empty TopSpace
for A, B being Subset of T st T is normal & A <> {} & A is closed & B is closed & A misses B holds
for b4 being Functional_Sequence of DYADIC,(bool the carrier of T) holds
( b4 is Rain of A,B iff for n being Element of NAT holds
( b4 . n is Drizzle of A,B,n & ( for r being Element of dom (b4 . n) holds (b4 . n) . r = (b4 . (n + 1)) . r ) ) );

definition
let x be Real;
assume A1: x in DYADIC ;
func inf_number_dyadic x ->  Element of NAT  means :Def3: :: URYSOHN3:def 3
( ( x in dyadic 0 implies it = 0 ) & ( it = 0 implies x in dyadic 0 ) & ( for n being Element of NAT st x in dyadic (n + 1) & not x in dyadic n holds
it = n + 1 ) );
existence
 ex b1 being Element of NAT st
( ( x in dyadic 0 implies b1 = 0 ) & ( b1 = 0 implies x in dyadic 0 ) & ( for n being Element of NAT st x in dyadic (n + 1) & not x in dyadic n holds
b1 = n + 1 ) )
proof
defpred S1[ Nat] means x in dyadic $1;
 ex s being Element of NAT st S1[s] by A1, URYSOHN1:def_2;
then A2: ex s being Nat st S1[s] ;
 ex q being Nat st
( S1[q] & ( for i being Nat st S1[i] holds
q <= i ) ) from NAT_1:sch_5(A2);
then consider q being Nat such that
A3: x in dyadic q and
A4: for i being Nat st x in dyadic i holds
q <= i ;
reconsider q = q as Element of NAT by ORDINAL1:def_12;
take  q ; ::_thesis: ( ( x in dyadic 0 implies q = 0 ) & ( q = 0 implies x in dyadic 0 ) & ( for n being Element of NAT st x in dyadic (n + 1) & not x in dyadic n holds
q = n + 1 ) )
 for n being Element of NAT st x in dyadic (n + 1) & not x in dyadic n holds
q = n + 1
proof
let n be Element of NAT ; ::_thesis: ( x in dyadic (n + 1) & not x in dyadic n implies q = n + 1 )
assume that
A5: x in dyadic (n + 1) and
A6: not x in dyadic n ; ::_thesis: q = n + 1
A7: n + 1 <= q
proof
assume  not n + 1 <= q ; ::_thesis: contradiction
then  q <= n by NAT_1:13;
then  dyadic q c= dyadic n by URYSOHN2:29;
hence  contradiction by A3, A6; ::_thesis: verum
end;
 q <= n + 1 by A4, A5;
hence  q = n + 1 by A7, XXREAL_0:1; ::_thesis: verum
end;
hence  ( ( x in dyadic 0 implies q = 0 ) & ( q = 0 implies x in dyadic 0 ) & ( for n being Element of NAT st x in dyadic (n + 1) & not x in dyadic n holds
q = n + 1 ) ) by A3, A4; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Element of NAT holds
not ( ( x in dyadic 0 implies b1 = 0 ) & ( b1 = 0 implies x in dyadic 0 ) & ( for n being Element of NAT st x in dyadic (n + 1) & not x in dyadic n holds
b1 = n + 1 ) & ( x in dyadic 0 implies b2 = 0 ) & ( b2 = 0 implies x in dyadic 0 ) & ( for n being Element of NAT st x in dyadic (n + 1) & not x in dyadic n holds
b2 = n + 1 ) & not b1 = b2 )
proof
let s1, s2 be Element of NAT ; ::_thesis: not ( ( x in dyadic 0 implies s1 = 0 ) & ( s1 = 0 implies x in dyadic 0 ) & ( for n being Element of NAT st x in dyadic (n + 1) & not x in dyadic n holds
s1 = n + 1 ) & ( x in dyadic 0 implies s2 = 0 ) & ( s2 = 0 implies x in dyadic 0 ) & ( for n being Element of NAT st x in dyadic (n + 1) & not x in dyadic n holds
s2 = n + 1 ) & not s1 = s2 )
assume that
A8: ( x in dyadic 0 iff s1 = 0 ) and
A9: for n being Element of NAT st x in dyadic (n + 1) & not x in dyadic n holds
s1 = n + 1 and
A10: ( x in dyadic 0 iff s2 = 0 ) and
A11: for n being Element of NAT st x in dyadic (n + 1) & not x in dyadic n holds
s2 = n + 1 ; ::_thesis: s1 = s2
percases ( s1 = 0 or 0 < s1 ) ;
suppose s1 = 0 ; ::_thesis: s1 = s2
hence  s1 = s2 by A8, A10; ::_thesis: verum
end;
supposeA12: 0 < s1 ; ::_thesis: s1 = s2
defpred S1[ Nat] means x in dyadic $1;
 ex s being Element of NAT st S1[s] by A1, URYSOHN1:def_2;
then A13: ex s being Nat st S1[s] ;
 ex q being Nat st
( S1[q] & ( for i being Nat st S1[i] holds
q <= i ) ) from NAT_1:sch_5(A13);
then consider q being Nat such that
A14: x in dyadic q and
A15: for i being Nat st x in dyadic i holds
q <= i ;
now__::_thesis:_(_(_q_=_0_&_s1_=_s2_)_or_(_0_<_q_&_s1_=_s2_)_)
percases ( q = 0 or 0 < q ) ;
case q = 0 ; ::_thesis: s1 = s2
hence  s1 = s2 by A8, A12, A14; ::_thesis: verum
end;
case 0 < q ; ::_thesis: s1 = s2
then consider m being Nat such that
A16: q = m + 1 by NAT_1:6;
reconsider m = m as Element of NAT by ORDINAL1:def_12;
A17: not x in dyadic m
proof
assume  x in dyadic m ; ::_thesis: contradiction
then  m + 1 <= m + 0 by A15, A16;
hence  contradiction by XREAL_1:6; ::_thesis: verum
end;
then  s1 = m + 1 by A9, A14, A16;
hence  s1 = s2 by A11, A14, A16, A17; ::_thesis: verum
end;
end;
end;
hence  s1 = s2 ; ::_thesis: verum
end;
end;
end;
end;

:: deftheorem Def3 defines inf_number_dyadic URYSOHN3:def_3_:_
 for x being Real st x in DYADIC holds
for b2 being Element of NAT holds
( b2 = inf_number_dyadic x iff ( ( x in dyadic 0 implies b2 = 0 ) & ( b2 = 0 implies x in dyadic 0 ) & ( for n being Element of NAT st x in dyadic (n + 1) & not x in dyadic n holds
b2 = n + 1 ) ) );

theorem Th5: :: URYSOHN3:5
for x being Real st x in DYADIC holds
x in dyadic (inf_number_dyadic x)
proof
let x be Real; ::_thesis: ( x in DYADIC implies x in dyadic (inf_number_dyadic x) )
set s = inf_number_dyadic x;
defpred S1[ Element of NAT ] means  not x in dyadic (((inf_number_dyadic x) + 1) + $1);
assume A1: x in DYADIC ; ::_thesis: x in dyadic (inf_number_dyadic x)
then consider k being Element of NAT  such that
A2: x in dyadic k by URYSOHN1:def_2;
A3: for i being Element of NAT st S1[i] holds
S1[i + 1]
proof
let i be Element of NAT ; ::_thesis: ( S1[i] implies S1[i + 1] )
assume A4: not x in dyadic (((inf_number_dyadic x) + 1) + i) ; ::_thesis: S1[i + 1]
assume  x in dyadic (((inf_number_dyadic x) + 1) + (i + 1)) ; ::_thesis: contradiction
then  x in dyadic ((((inf_number_dyadic x) + 1) + i) + 1) ;
then  (inf_number_dyadic x) + 0 = (inf_number_dyadic x) + (i + 2) by A1, A4, Def3;
hence  contradiction ; ::_thesis: verum
end;
assume A5: not x in dyadic (inf_number_dyadic x) ; ::_thesis: contradiction
A6: inf_number_dyadic x < k
proof
assume  not inf_number_dyadic x < k ; ::_thesis: contradiction
then  dyadic k c= dyadic (inf_number_dyadic x) by URYSOHN2:29;
hence  contradiction by A5, A2; ::_thesis: verum
end;
then consider i being Nat such that
A7: k = i + 1 by NAT_1:6;
 inf_number_dyadic x <= i by A6, A7, NAT_1:13;
then consider m being Nat such that
A8: i = (inf_number_dyadic x) + m by NAT_1:10;
reconsider m = m as Element of NAT by ORDINAL1:def_12;
A9: S1[ 0 ] by A1, A5, Def3;
 for i being Element of NAT holds S1[i] from NAT_1:sch_1(A9, A3);
then  not x in dyadic (((inf_number_dyadic x) + 1) + m) ;
hence  contradiction by A2, A7, A8; ::_thesis: verum
end;

theorem Th6: :: URYSOHN3:6
for x being Real st x in DYADIC holds
for n being Element of NAT st inf_number_dyadic x <= n holds
x in dyadic n
proof
let x be Real; ::_thesis: ( x in DYADIC implies for n being Element of NAT st inf_number_dyadic x <= n holds
x in dyadic n )
assume  x in DYADIC ; ::_thesis: for n being Element of NAT st inf_number_dyadic x <= n holds
x in dyadic n
then A1: x in dyadic (inf_number_dyadic x) by Th5;
let n be Element of NAT ; ::_thesis: ( inf_number_dyadic x <= n implies x in dyadic n )
assume  inf_number_dyadic x <= n ; ::_thesis: x in dyadic n
then  dyadic (inf_number_dyadic x) c= dyadic n by URYSOHN2:29;
hence  x in dyadic n by A1; ::_thesis: verum
end;

theorem Th7: :: URYSOHN3:7
for x being Real
for n being Element of NAT st x in dyadic n holds
inf_number_dyadic x <= n
proof
let x be Real; ::_thesis: for n being Element of NAT st x in dyadic n holds
inf_number_dyadic x <= n
let n be Element of NAT ; ::_thesis: ( x in dyadic n implies inf_number_dyadic x <= n )
A1: dyadic n c= DYADIC by URYSOHN2:23;
defpred S1[ Nat] means x in dyadic $1;
assume A2: x in dyadic n ; ::_thesis: inf_number_dyadic x <= n
then A3: ex s being Nat st S1[s] ;
 ex q being Nat st
( S1[q] & ( for i being Nat st S1[i] holds
q <= i ) ) from NAT_1:sch_5(A3);
then consider q being Nat such that
A4: x in dyadic q and
A5: for i being Nat st x in dyadic i holds
q <= i ;
A6: q <= n by A2, A5;
now__::_thesis:_(_(_q_=_0_&_inf_number_dyadic_x_<=_n_)_or_(_0_<_q_&_inf_number_dyadic_x_<=_n_)_)
percases ( q = 0 or 0 < q ) ;
case q = 0 ; ::_thesis: inf_number_dyadic x <= n
hence  inf_number_dyadic x <= n by A2, A1, A4, Def3; ::_thesis: verum
end;
case 0 < q ; ::_thesis: inf_number_dyadic x <= n
then consider m being Nat such that
A7: q = m + 1 by NAT_1:6;
reconsider m = m as Element of NAT by ORDINAL1:def_12;
 not x in dyadic m
proof
assume  x in dyadic m ; ::_thesis: contradiction
then  m + 1 <= m + 0 by A5, A7;
hence  contradiction by XREAL_1:6; ::_thesis: verum
end;
hence  inf_number_dyadic x <= n by A2, A1, A4, A6, A7, Def3; ::_thesis: verum
end;
end;
end;
hence  inf_number_dyadic x <= n ; ::_thesis: verum
end;

theorem Th8: :: URYSOHN3:8
for T being non empty normal TopSpace
for A, B being closed Subset of T st A <> {} & A misses B holds
for G being Rain of A,B
for x being Real st x in DYADIC holds
for n being Element of NAT holds (G . (inf_number_dyadic x)) . x = (G . ((inf_number_dyadic x) + n)) . x
proof
let T be non empty normal TopSpace; ::_thesis: for A, B being closed Subset of T st A <> {} & A misses B holds
for G being Rain of A,B
for x being Real st x in DYADIC holds
for n being Element of NAT holds (G . (inf_number_dyadic x)) . x = (G . ((inf_number_dyadic x) + n)) . x
let A, B be closed Subset of T; ::_thesis: ( A <> {} & A misses B implies for G being Rain of A,B
for x being Real st x in DYADIC holds
for n being Element of NAT holds (G . (inf_number_dyadic x)) . x = (G . ((inf_number_dyadic x) + n)) . x )
assume A1: ( A <> {} & A misses B ) ; ::_thesis: for G being Rain of A,B
for x being Real st x in DYADIC holds
for n being Element of NAT holds (G . (inf_number_dyadic x)) . x = (G . ((inf_number_dyadic x) + n)) . x
let G be Rain of A,B; ::_thesis: for x being Real st x in DYADIC holds
for n being Element of NAT holds (G . (inf_number_dyadic x)) . x = (G . ((inf_number_dyadic x) + n)) . x
let x be Real; ::_thesis: ( x in DYADIC implies for n being Element of NAT holds (G . (inf_number_dyadic x)) . x = (G . ((inf_number_dyadic x) + n)) . x )
set s = inf_number_dyadic x;
defpred S1[ Element of NAT ] means (G . (inf_number_dyadic x)) . x = (G . ((inf_number_dyadic x) + $1)) . x;
assume A2: x in DYADIC ; ::_thesis: for n being Element of NAT holds (G . (inf_number_dyadic x)) . x = (G . ((inf_number_dyadic x) + n)) . x
A3: for n being Element of NAT st S1[n] holds
S1[n + 1]
proof
let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] )
assume A4: (G . (inf_number_dyadic x)) . x = (G . ((inf_number_dyadic x) + n)) . x ; ::_thesis: S1[n + 1]
 inf_number_dyadic x <= (inf_number_dyadic x) + (n + 1) by NAT_1:11;
then A5: x in dyadic (((inf_number_dyadic x) + n) + 1) by A2, Th6;
 G . ((inf_number_dyadic x) + n) is Drizzle of A,B,(inf_number_dyadic x) + n by A1, Def2;
then A6: dom (G . ((inf_number_dyadic x) + n)) = dyadic ((inf_number_dyadic x) + n) by FUNCT_2:def_1;
 x in dyadic ((inf_number_dyadic x) + n) by A2, Th6, NAT_1:11;
hence  S1[n + 1] by A1, A4, A5, A6, Def2; ::_thesis: verum
end;
A7: S1[ 0 ] ;
 for i being Element of NAT holds S1[i] from NAT_1:sch_1(A7, A3);
hence  for n being Element of NAT holds (G . (inf_number_dyadic x)) . x = (G . ((inf_number_dyadic x) + n)) . x ; ::_thesis: verum
end;

theorem Th9: :: URYSOHN3:9
for T being non empty normal TopSpace
for A, B being closed Subset of T st A <> {} & A misses B holds
for G being Rain of A,B
for x being Real st x in DYADIC holds
ex y being Subset of T st
for n being Element of NAT st x in dyadic n holds
y = (G . n) . x
proof
let T be non empty normal TopSpace; ::_thesis: for A, B being closed Subset of T st A <> {} & A misses B holds
for G being Rain of A,B
for x being Real st x in DYADIC holds
ex y being Subset of T st
for n being Element of NAT st x in dyadic n holds
y = (G . n) . x
let A, B be closed Subset of T; ::_thesis: ( A <> {} & A misses B implies for G being Rain of A,B
for x being Real st x in DYADIC holds
ex y being Subset of T st
for n being Element of NAT st x in dyadic n holds
y = (G . n) . x )
assume A1: ( A <> {} & A misses B ) ; ::_thesis: for G being Rain of A,B
for x being Real st x in DYADIC holds
ex y being Subset of T st
for n being Element of NAT st x in dyadic n holds
y = (G . n) . x
let G be Rain of A,B; ::_thesis: for x being Real st x in DYADIC holds
ex y being Subset of T st
for n being Element of NAT st x in dyadic n holds
y = (G . n) . x
let x be Real; ::_thesis: ( x in DYADIC implies ex y being Subset of T st
for n being Element of NAT st x in dyadic n holds
y = (G . n) . x )
assume A2: x in DYADIC ; ::_thesis: ex y being Subset of T st
for n being Element of NAT st x in dyadic n holds
y = (G . n) . x
reconsider s = inf_number_dyadic x as Element of NAT ;
 G . s is Drizzle of A,B,s by A1, Def2;
then reconsider y = (G . s) . x as Subset of T by A2, Th5, FUNCT_2:5;
take  y ; ::_thesis: for n being Element of NAT st x in dyadic n holds
y = (G . n) . x
let n be Element of NAT ; ::_thesis: ( x in dyadic n implies y = (G . n) . x )
assume  x in dyadic n ; ::_thesis: y = (G . n) . x
then consider m being Nat such that
A3: n = s + m by Th7, NAT_1:10;
 m in NAT by ORDINAL1:def_12;
hence  y = (G . n) . x by A1, A2, A3, Th8; ::_thesis: verum
end;

theorem Th10: :: URYSOHN3:10
for T being non empty normal TopSpace
for A, B being closed Subset of T st A <> {} & A misses B holds
for G being Rain of A,B ex F being Function of DOM,(bool the carrier of T) st
for x being Real st x in DOM holds
( ( x in halfline 0 implies F . x = {} ) & ( x in right_open_halfline 1 implies F . x = the carrier of T ) & ( x in DYADIC implies for n being Element of NAT st x in dyadic n holds
F . x = (G . n) . x ) )
proof
let T be non empty normal TopSpace; ::_thesis: for A, B being closed Subset of T st A <> {} & A misses B holds
for G being Rain of A,B ex F being Function of DOM,(bool the carrier of T) st
for x being Real st x in DOM holds
( ( x in halfline 0 implies F . x = {} ) & ( x in right_open_halfline 1 implies F . x = the carrier of T ) & ( x in DYADIC implies for n being Element of NAT st x in dyadic n holds
F . x = (G . n) . x ) )
let A, B be closed Subset of T; ::_thesis: ( A <> {} & A misses B implies for G being Rain of A,B ex F being Function of DOM,(bool the carrier of T) st
for x being Real st x in DOM holds
( ( x in halfline 0 implies F . x = {} ) & ( x in right_open_halfline 1 implies F . x = the carrier of T ) & ( x in DYADIC implies for n being Element of NAT st x in dyadic n holds
F . x = (G . n) . x ) ) )
assume A1: ( A <> {} & A misses B ) ; ::_thesis: for G being Rain of A,B ex F being Function of DOM,(bool the carrier of T) st
for x being Real st x in DOM holds
( ( x in halfline 0 implies F . x = {} ) & ( x in right_open_halfline 1 implies F . x = the carrier of T ) & ( x in DYADIC implies for n being Element of NAT st x in dyadic n holds
F . x = (G . n) . x ) )
let G be Rain of A,B; ::_thesis: ex F being Function of DOM,(bool the carrier of T) st
for x being Real st x in DOM holds
( ( x in halfline 0 implies F . x = {} ) & ( x in right_open_halfline 1 implies F . x = the carrier of T ) & ( x in DYADIC implies for n being Element of NAT st x in dyadic n holds
F . x = (G . n) . x ) )
defpred S1[ Element of DOM , set ] means ( ( $1 in halfline 0 implies $2 = {} ) & ( $1 in right_open_halfline 1 implies $2 = the carrier of T ) & ( $1 in DYADIC implies for n being Element of NAT st $1 in dyadic n holds
$2 = (G . n) . $1 ) );
A2: for x being Element of DOM ex y being Subset of T st S1[x,y]
proof
reconsider a = 0 , b = 1 as R_eal by XXREAL_0:def_1;
let x be Element of DOM ; ::_thesis: ex y being Subset of T st S1[x,y]
A3: ( x in (halfline 0) \/ DYADIC or x in right_open_halfline 1 ) by URYSOHN1:def_3, XBOOLE_0:def_3;
percases ( x in halfline 0 or x in DYADIC or x in right_open_halfline 1 ) by A3, XBOOLE_0:def_3;
supposeA4: x in halfline 0 ; ::_thesis: ex y being Subset of T st S1[x,y]
A5: ( not x in right_open_halfline 1 & not x in DYADIC )
proof
assume A6: ( x in right_open_halfline 1 or x in DYADIC ) ; ::_thesis: contradiction
percases ( x in right_open_halfline 1 or x in DYADIC ) by A6;
suppose x in right_open_halfline 1 ; ::_thesis: contradiction
then  1 < x by XXREAL_1:235;
hence  contradiction by A4, XXREAL_1:233; ::_thesis: verum
end;
supposeA7: x in DYADIC ; ::_thesis: contradiction
reconsider x = x as R_eal by XXREAL_0:def_1;
 a <= x by A7, URYSOHN2:28, XXREAL_1:1;
hence  contradiction by A4, XXREAL_1:233; ::_thesis: verum
end;
end;
end;
reconsider s = {} as Subset of T by XBOOLE_1:2;
 s = s ;
hence  ex y being Subset of T st S1[x,y] by A5; ::_thesis: verum
end;
supposeA8: x in DYADIC ; ::_thesis: ex y being Subset of T st S1[x,y]
A9: not x in halfline 0
proof
assume A10: x in halfline 0 ; ::_thesis: contradiction
reconsider x = x as R_eal by XXREAL_0:def_1;
 a <= x by A8, URYSOHN2:28, XXREAL_1:1;
hence  contradiction by A10, XXREAL_1:233; ::_thesis: verum
end;
A11: not x in right_open_halfline 1
proof
assume A12: x in right_open_halfline 1 ; ::_thesis: contradiction
reconsider x = x as R_eal by XXREAL_0:def_1;
 x <= b by A8, URYSOHN2:28, XXREAL_1:1;
hence  contradiction by A12, XXREAL_1:235; ::_thesis: verum
end;
 ex s being Subset of T st
for n being Element of NAT st x in dyadic n holds
s = (G . n) . x by A1, A8, Th9;
hence  ex y being Subset of T st S1[x,y] by A11, A9; ::_thesis: verum
end;
supposeA13: x in right_open_halfline 1 ; ::_thesis: ex y being Subset of T st S1[x,y]
A14: ( not x in halfline 0 & not x in DYADIC )
proof
assume A15: ( x in halfline 0 or x in DYADIC ) ; ::_thesis: contradiction
percases ( x in halfline 0 or x in DYADIC ) by A15;
suppose x in halfline 0 ; ::_thesis: contradiction
then  x < 0 by XXREAL_1:233;
hence  contradiction by A13, XXREAL_1:235; ::_thesis: verum
end;
supposeA16: x in DYADIC ; ::_thesis: contradiction
reconsider x = x as R_eal by XXREAL_0:def_1;
 x <= b by A16, URYSOHN2:28, XXREAL_1:1;
hence  contradiction by A13, XXREAL_1:235; ::_thesis: verum
end;
end;
end;
 the carrier of T c= the carrier of T ;
then reconsider s = the carrier of T as Subset of T ;
 s = s ;
hence  ex y being Subset of T st S1[x,y] by A14; ::_thesis: verum
end;
end;
end;
 ex F being Function of DOM,(bool the carrier of T) st
for x being Element of DOM holds S1[x,F . x] from FUNCT_2:sch_3(A2);
then consider F being Function of DOM,(bool the carrier of T) such that
A17: for x being Element of DOM holds S1[x,F . x] ;
take  F ; ::_thesis: for x being Real st x in DOM holds
( ( x in halfline 0 implies F . x = {} ) & ( x in right_open_halfline 1 implies F . x = the carrier of T ) & ( x in DYADIC implies for n being Element of NAT st x in dyadic n holds
F . x = (G . n) . x ) )
thus  for x being Real st x in DOM holds
( ( x in halfline 0 implies F . x = {} ) & ( x in right_open_halfline 1 implies F . x = the carrier of T ) & ( x in DYADIC implies for n being Element of NAT st x in dyadic n holds
F . x = (G . n) . x ) ) by A17; ::_thesis: verum
end;

definition
let T be non empty TopSpace;
let A, B be Subset of T;
assume A1: ( T is normal & A <> {} & A is closed & B is closed & A misses B ) ;
let R be Rain of A,B;
func Tempest R ->  Function of DOM,(bool the carrier of T) means :Def4: :: URYSOHN3:def 4
 for x being Real st x in DOM holds
( ( x in halfline 0 implies it . x = {} ) & ( x in right_open_halfline 1 implies it . x = the carrier of T ) & ( x in DYADIC implies for n being Element of NAT st x in dyadic n holds
it . x = (R . n) . x ) );
existence
 ex b1 being Function of DOM,(bool the carrier of T) st
for x being Real st x in DOM holds
( ( x in halfline 0 implies b1 . x = {} ) & ( x in right_open_halfline 1 implies b1 . x = the carrier of T ) & ( x in DYADIC implies for n being Element of NAT st x in dyadic n holds
b1 . x = (R . n) . x ) ) by A1, Th10;
uniqueness
 for b1, b2 being Function of DOM,(bool the carrier of T) st ( for x being Real st x in DOM holds
( ( x in halfline 0 implies b1 . x = {} ) & ( x in right_open_halfline 1 implies b1 . x = the carrier of T ) & ( x in DYADIC implies for n being Element of NAT st x in dyadic n holds
b1 . x = (R . n) . x ) ) ) & ( for x being Real st x in DOM holds
( ( x in halfline 0 implies b2 . x = {} ) & ( x in right_open_halfline 1 implies b2 . x = the carrier of T ) & ( x in DYADIC implies for n being Element of NAT st x in dyadic n holds
b2 . x = (R . n) . x ) ) ) holds
b1 = b2
proof
let G1, G2 be Function of DOM,(bool the carrier of T); ::_thesis: ( ( for x being Real st x in DOM holds
( ( x in halfline 0 implies G1 . x = {} ) & ( x in right_open_halfline 1 implies G1 . x = the carrier of T ) & ( x in DYADIC implies for n being Element of NAT st x in dyadic n holds
G1 . x = (R . n) . x ) ) ) & ( for x being Real st x in DOM holds
( ( x in halfline 0 implies G2 . x = {} ) & ( x in right_open_halfline 1 implies G2 . x = the carrier of T ) & ( x in DYADIC implies for n being Element of NAT st x in dyadic n holds
G2 . x = (R . n) . x ) ) ) implies G1 = G2 )
assume that
A2: for x being Real st x in DOM holds
( ( x in halfline 0 implies G1 . x = {} ) & ( x in right_open_halfline 1 implies G1 . x = the carrier of T ) & ( x in DYADIC implies for n being Element of NAT st x in dyadic n holds
G1 . x = (R . n) . x ) ) and
A3: for x being Real st x in DOM holds
( ( x in halfline 0 implies G2 . x = {} ) & ( x in right_open_halfline 1 implies G2 . x = the carrier of T ) & ( x in DYADIC implies for n being Element of NAT st x in dyadic n holds
G2 . x = (R . n) . x ) ) ; ::_thesis: G1 = G2
 for x being set st x in DOM holds
G1 . x = G2 . x
proof
let x be set ; ::_thesis: ( x in DOM implies G1 . x = G2 . x )
assume A4: x in DOM ; ::_thesis: G1 . x = G2 . x
then reconsider x = x as Real ;
A5: ( x in (halfline 0) \/ DYADIC or x in right_open_halfline 1 ) by A4, URYSOHN1:def_3, XBOOLE_0:def_3;
percases ( x in halfline 0 or x in right_open_halfline 1 or x in DYADIC ) by A5, XBOOLE_0:def_3;
supposeA6: x in halfline 0 ; ::_thesis: G1 . x = G2 . x
then  G1 . x = {} by A2, A4;
hence  G1 . x = G2 . x by A3, A4, A6; ::_thesis: verum
end;
supposeA7: x in right_open_halfline 1 ; ::_thesis: G1 . x = G2 . x
then  G1 . x = the carrier of T by A2, A4;
hence  G1 . x = G2 . x by A3, A4, A7; ::_thesis: verum
end;
supposeA8: x in DYADIC ; ::_thesis: G1 . x = G2 . x
then consider n being Element of NAT  such that
A9: x in dyadic n by URYSOHN1:def_2;
 G1 . x = (R . n) . x by A2, A4, A8, A9;
hence  G1 . x = G2 . x by A3, A4, A8, A9; ::_thesis: verum
end;
end;
end;
hence  G1 = G2 by FUNCT_2:12; ::_thesis: verum
end;
end;

:: deftheorem Def4 defines Tempest URYSOHN3:def_4_:_
 for T being non empty TopSpace
for A, B being Subset of T st T is normal & A <> {} & A is closed & B is closed & A misses B holds
for R being Rain of A,B
for b5 being Function of DOM,(bool the carrier of T) holds
( b5 = Tempest R iff for x being Real st x in DOM holds
( ( x in halfline 0 implies b5 . x = {} ) & ( x in right_open_halfline 1 implies b5 . x = the carrier of T ) & ( x in DYADIC implies for n being Element of NAT st x in dyadic n holds
b5 . x = (R . n) . x ) ) );

definition
let X be non empty set ;
let T be TopSpace;
let F be Function of X,(bool the carrier of T);
let x be Element of X;
:: original: .
redefine funcF . x ->  Subset of T;
correctness
coherence
F . x is Subset of T;
proof
 F . x c= the carrier of T ;
hence  F . x is Subset of T ; ::_thesis: verum
end;
end;

theorem Th11: :: URYSOHN3:11
for T being non empty normal TopSpace
for A, B being closed Subset of T st A <> {} & A misses B holds
for G being Rain of A,B
for r being Real
for C being Subset of T st C = (Tempest G) . r & r in DOM holds
C is open
proof
let T be non empty normal TopSpace; ::_thesis: for A, B being closed Subset of T st A <> {} & A misses B holds
for G being Rain of A,B
for r being Real
for C being Subset of T st C = (Tempest G) . r & r in DOM holds
C is open
let A, B be closed Subset of T; ::_thesis: ( A <> {} & A misses B implies for G being Rain of A,B
for r being Real
for C being Subset of T st C = (Tempest G) . r & r in DOM holds
C is open )
assume A1: ( A <> {} & A misses B ) ; ::_thesis: for G being Rain of A,B
for r being Real
for C being Subset of T st C = (Tempest G) . r & r in DOM holds
C is open
let G be Rain of A,B; ::_thesis: for r being Real
for C being Subset of T st C = (Tempest G) . r & r in DOM holds
C is open
let r be Real; ::_thesis: for C being Subset of T st C = (Tempest G) . r & r in DOM holds
C is open
let C be Subset of T; ::_thesis: ( C = (Tempest G) . r & r in DOM implies C is open )
assume that
A2: C = (Tempest G) . r and
A3: r in DOM ; ::_thesis: C is open
A4: ( r in (halfline 0) \/ DYADIC or r in right_open_halfline 1 ) by A3, URYSOHN1:def_3, XBOOLE_0:def_3;
percases ( r in halfline 0 or r in DYADIC or r in right_open_halfline 1 ) by A4, XBOOLE_0:def_3;
suppose r in halfline 0 ; ::_thesis: C is open
then  C = {} by A1, A2, A3, Def4;
then  C in the topology of T by PRE_TOPC:1;
hence  C is open by PRE_TOPC:def_2; ::_thesis: verum
end;
supposeA5: r in DYADIC ; ::_thesis: C is open
then consider n being Element of NAT  such that
A6: r in dyadic n by URYSOHN1:def_2;
reconsider D = G . n as Drizzle of A,B,n by A1, Def2;
A7: for r1, r2 being Element of dyadic n st r1 < r2 holds
( D . r1 is open & D . r2 is open & Cl (D . r1) c= D . r2 & A c= D . 0 & B = ([#] T) \ (D . 1) ) by A1, Def1;
A8: (Tempest G) . r = (G . n) . r by A1, A3, A5, A6, Def4;
now__::_thesis:_(_(_r_=_0_&_C_is_open_)_or_(_0_<_r_&_C_is_open_)_)
percases ( r = 0 or 0 < r ) by A6, URYSOHN1:1;
caseA9: r = 0 ; ::_thesis: C is open
then reconsider r = r as Element of dyadic n by URYSOHN1:6;
 ( 1 is Element of dyadic n & D . r = C ) by A1, A2, A3, A5, Def4, URYSOHN1:6;
hence  C is open by A1, A9, Def1; ::_thesis: verum
end;
caseA10: 0 < r ; ::_thesis: C is open
 0 in dyadic n by URYSOHN1:6;
hence  C is open by A2, A6, A8, A7, A10; ::_thesis: verum
end;
end;
end;
hence  C is open ; ::_thesis: verum
end;
supposeA11: r in right_open_halfline 1 ; ::_thesis: C is open
A12: the carrier of T in the topology of T by PRE_TOPC:def_1;
 C = the carrier of T by A1, A2, A3, A11, Def4;
hence  C is open by A12, PRE_TOPC:def_2; ::_thesis: verum
end;
end;
end;

theorem Th12: :: URYSOHN3:12
for T being non empty normal TopSpace
for A, B being closed Subset of T st A <> {} & A misses B holds
for G being Rain of A,B
for r1, r2 being Real st r1 in DOM & r2 in DOM & r1 < r2 holds
for C being Subset of T st C = (Tempest G) . r1 holds
Cl C c= (Tempest G) . r2
proof
let T be non empty normal TopSpace; ::_thesis: for A, B being closed Subset of T st A <> {} & A misses B holds
for G being Rain of A,B
for r1, r2 being Real st r1 in DOM & r2 in DOM & r1 < r2 holds
for C being Subset of T st C = (Tempest G) . r1 holds
Cl C c= (Tempest G) . r2
let A, B be closed Subset of T; ::_thesis: ( A <> {} & A misses B implies for G being Rain of A,B
for r1, r2 being Real st r1 in DOM & r2 in DOM & r1 < r2 holds
for C being Subset of T st C = (Tempest G) . r1 holds
Cl C c= (Tempest G) . r2 )
assume A1: ( A <> {} & A misses B ) ; ::_thesis: for G being Rain of A,B
for r1, r2 being Real st r1 in DOM & r2 in DOM & r1 < r2 holds
for C being Subset of T st C = (Tempest G) . r1 holds
Cl C c= (Tempest G) . r2
let G be Rain of A,B; ::_thesis: for r1, r2 being Real st r1 in DOM & r2 in DOM & r1 < r2 holds
for C being Subset of T st C = (Tempest G) . r1 holds
Cl C c= (Tempest G) . r2
let r1, r2 be Real; ::_thesis: ( r1 in DOM & r2 in DOM & r1 < r2 implies for C being Subset of T st C = (Tempest G) . r1 holds
Cl C c= (Tempest G) . r2 )
assume that
A2: r1 in DOM and
A3: r2 in DOM and
A4: r1 < r2 ; ::_thesis: for C being Subset of T st C = (Tempest G) . r1 holds
Cl C c= (Tempest G) . r2
A5: ( r1 in (halfline 0) \/ DYADIC or r1 in right_open_halfline 1 ) by A2, URYSOHN1:def_3, XBOOLE_0:def_3;
A6: ( r2 in (halfline 0) \/ DYADIC or r2 in right_open_halfline 1 ) by A3, URYSOHN1:def_3, XBOOLE_0:def_3;
let C be Subset of T; ::_thesis: ( C = (Tempest G) . r1 implies Cl C c= (Tempest G) . r2 )
assume A7: C = (Tempest G) . r1 ; ::_thesis: Cl C c= (Tempest G) . r2
percases ( ( r1 in halfline 0 & r2 in halfline 0 ) or ( r1 in DYADIC & r2 in halfline 0 ) or ( r1 in right_open_halfline 1 & r2 in halfline 0 ) or ( r1 in halfline 0 & r2 in DYADIC ) or ( r1 in DYADIC & r2 in DYADIC ) or ( r1 in right_open_halfline 1 & r2 in DYADIC ) or ( r1 in halfline 0 & r2 in right_open_halfline 1 ) or ( r1 in DYADIC & r2 in right_open_halfline 1 ) or ( r1 in right_open_halfline 1 & r2 in right_open_halfline 1 ) ) by A5, A6, XBOOLE_0:def_3;
supposeA8: ( r1 in halfline 0 & r2 in halfline 0 ) ; ::_thesis: Cl C c= (Tempest G) . r2
 C = {} by A1, A2, A7, A8, Def4;
then  Cl C = {} by PRE_TOPC:22;
hence  Cl C c= (Tempest G) . r2 by XBOOLE_1:2; ::_thesis: verum
end;
suppose ( r1 in DYADIC & r2 in halfline 0 ) ; ::_thesis: Cl C c= (Tempest G) . r2
then  ( r2 < 0 & ex s being Element of NAT st r1 in dyadic s ) by URYSOHN1:def_2, XXREAL_1:233;
hence  Cl C c= (Tempest G) . r2 by A4, URYSOHN1:1; ::_thesis: verum
end;
supposeA9: ( r1 in right_open_halfline 1 & r2 in halfline 0 ) ; ::_thesis: Cl C c= (Tempest G) . r2
then  1 < r1 by XXREAL_1:235;
hence  Cl C c= (Tempest G) . r2 by A4, A9, XXREAL_1:233; ::_thesis: verum
end;
supposeA10: ( r1 in halfline 0 & r2 in DYADIC ) ; ::_thesis: Cl C c= (Tempest G) . r2
 C = {} by A1, A2, A7, A10, Def4;
then  Cl C = {} by PRE_TOPC:22;
hence  Cl C c= (Tempest G) . r2 by XBOOLE_1:2; ::_thesis: verum
end;
supposeA11: ( r1 in DYADIC & r2 in DYADIC ) ; ::_thesis: Cl C c= (Tempest G) . r2
then consider n2 being Element of NAT  such that
A12: r2 in dyadic n2 by URYSOHN1:def_2;
consider n1 being Element of NAT  such that
A13: r1 in dyadic n1 by A11, URYSOHN1:def_2;
set n = n1 + n2;
A14: dyadic n1 c= dyadic (n1 + n2) by NAT_1:11, URYSOHN2:29;
then A15: (Tempest G) . r1 = (G . (n1 + n2)) . r1 by A1, A2, A11, A13, Def4;
 dyadic n2 c= dyadic (n1 + n2) by NAT_1:11, URYSOHN2:29;
then reconsider r1 = r1, r2 = r2 as Element of dyadic (n1 + n2) by A13, A12, A14;
reconsider D = G . (n1 + n2) as Drizzle of A,B,n1 + n2 by A1, Def2;
 Cl (D . r1) c= D . r2 by A1, A4, Def1;
hence  Cl C c= (Tempest G) . r2 by A1, A3, A7, A11, A15, Def4; ::_thesis: verum
end;
supposeA16: ( r1 in right_open_halfline 1 & r2 in DYADIC ) ; ::_thesis: Cl C c= (Tempest G) . r2
then  ex s being Element of NAT st r2 in dyadic s by URYSOHN1:def_2;
then A17: r2 <= 1 by URYSOHN1:1;
 1 < r1 by A16, XXREAL_1:235;
hence  Cl C c= (Tempest G) . r2 by A4, A17, XXREAL_0:2; ::_thesis: verum
end;
supposeA18: ( r1 in halfline 0 & r2 in right_open_halfline 1 ) ; ::_thesis: Cl C c= (Tempest G) . r2
 C = {} by A1, A2, A7, A18, Def4;
then  Cl C = {} by PRE_TOPC:22;
hence  Cl C c= (Tempest G) . r2 by XBOOLE_1:2; ::_thesis: verum
end;
suppose ( r1 in DYADIC & r2 in right_open_halfline 1 ) ; ::_thesis: Cl C c= (Tempest G) . r2
then  (Tempest G) . r2 = the carrier of T by A1, A3, Def4;
hence  Cl C c= (Tempest G) . r2 ; ::_thesis: verum
end;
suppose ( r1 in right_open_halfline 1 & r2 in right_open_halfline 1 ) ; ::_thesis: Cl C c= (Tempest G) . r2
then  (Tempest G) . r2 = the carrier of T by A1, A3, Def4;
hence  Cl C c= (Tempest G) . r2 ; ::_thesis: verum
end;
end;
end;

definition
let T be non empty TopSpace;
let A, B be Subset of T;
let G be Rain of A,B;
let p be Point of T;
func Rainbow (p,G) ->  Subset of ExtREAL means :Def5: :: URYSOHN3:def 5
 for x being set holds
( x in it iff ( x in DYADIC & ( for s being Real st s = x holds
not p in (Tempest G) . s ) ) );
existence
 ex b1 being Subset of ExtREAL st
for x being set holds
( x in b1 iff ( x in DYADIC & ( for s being Real st s = x holds
not p in (Tempest G) . s ) ) )
proof
defpred S1[ set ] means  for s being Real st s = $1 holds
not p in (Tempest G) . s;
 ex X being set st
for x being set holds
( x in X iff ( x in DYADIC & S1[x] ) ) from XBOOLE_0:sch_1();
then consider R being set  such that
A1: for x being set holds
( x in R iff ( x in DYADIC & S1[x] ) ) ;
 R c= REAL
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in R or x in REAL )
assume  x in R ; ::_thesis: x in REAL
then  x in DYADIC by A1;
hence  x in REAL ; ::_thesis: verum
end;
then reconsider R = R as Subset of ExtREAL by NUMBERS:31, XBOOLE_1:1;
take  R ; ::_thesis: for x being set holds
( x in R iff ( x in DYADIC & ( for s being Real st s = x holds
not p in (Tempest G) . s ) ) )
thus  for x being set holds
( x in R iff ( x in DYADIC & ( for s being Real st s = x holds
not p in (Tempest G) . s ) ) ) by A1; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Subset of ExtREAL st ( for x being set holds
( x in b1 iff ( x in DYADIC & ( for s being Real st s = x holds
not p in (Tempest G) . s ) ) ) ) & ( for x being set holds
( x in b2 iff ( x in DYADIC & ( for s being Real st s = x holds
not p in (Tempest G) . s ) ) ) ) holds
b1 = b2
proof
let R1, R2 be Subset of ExtREAL; ::_thesis: ( ( for x being set holds
( x in R1 iff ( x in DYADIC & ( for s being Real st s = x holds
not p in (Tempest G) . s ) ) ) ) & ( for x being set holds
( x in R2 iff ( x in DYADIC & ( for s being Real st s = x holds
not p in (Tempest G) . s ) ) ) ) implies R1 = R2 )
assume that
A2: for x being set holds
( x in R1 iff ( x in DYADIC & ( for s being Real st s = x holds
not p in (Tempest G) . s ) ) ) and
A3: for x being set holds
( x in R2 iff ( x in DYADIC & ( for s being Real st s = x holds
not p in (Tempest G) . s ) ) ) ; ::_thesis: R1 = R2
 for x being set holds
( x in R1 iff x in R2 )
proof
let x be set ; ::_thesis: ( x in R1 iff x in R2 )
hereby  ::_thesis: ( x in R2 implies x in R1 )
assume  x in R1 ; ::_thesis: x in R2
then  ( x in DYADIC & ( for s being Real st s = x holds
not p in (Tempest G) . s ) ) by A2;
hence  x in R2 by A3; ::_thesis: verum
end;
assume  x in R2 ; ::_thesis: x in R1
then  ( x in DYADIC & ( for s being Real st s = x holds
not p in (Tempest G) . s ) ) by A3;
hence  x in R1 by A2; ::_thesis: verum
end;
hence  R1 = R2 by TARSKI:1; ::_thesis: verum
end;
end;

:: deftheorem Def5 defines Rainbow URYSOHN3:def_5_:_
 for T being non empty TopSpace
for A, B being Subset of T
for G being Rain of A,B
for p being Point of T
for b6 being Subset of ExtREAL holds
( b6 = Rainbow (p,G) iff for x being set holds
( x in b6 iff ( x in DYADIC & ( for s being Real st s = x holds
not p in (Tempest G) . s ) ) ) );

theorem Th13: :: URYSOHN3:13
for T being non empty TopSpace
for A, B being Subset of T
for G being Rain of A,B
for p being Point of T holds Rainbow (p,G) c= DYADIC
proof
let T be non empty TopSpace; ::_thesis: for A, B being Subset of T
for G being Rain of A,B
for p being Point of T holds Rainbow (p,G) c= DYADIC
let A, B be Subset of T; ::_thesis: for G being Rain of A,B
for p being Point of T holds Rainbow (p,G) c= DYADIC
let G be Rain of A,B; ::_thesis: for p being Point of T holds Rainbow (p,G) c= DYADIC
let p be Point of T; ::_thesis: Rainbow (p,G) c= DYADIC
 for x being set st x in Rainbow (p,G) holds
x in DYADIC by Def5;
hence  Rainbow (p,G) c= DYADIC by TARSKI:def_3; ::_thesis: verum
end;

definition
let T be non empty TopSpace;
let A, B be Subset of T;
let R be Rain of A,B;
func Thunder R ->  Function of T,R^1 means :Def6: :: URYSOHN3:def 6
 for p being Point of T holds
( ( Rainbow (p,R) = {} implies it . p = 0 ) & ( for S being non empty Subset of ExtREAL st S = Rainbow (p,R) holds
it . p = sup S ) );
existence
 ex b1 being Function of T,R^1 st
for p being Point of T holds
( ( Rainbow (p,R) = {} implies b1 . p = 0 ) & ( for S being non empty Subset of ExtREAL st S = Rainbow (p,R) holds
b1 . p = sup S ) )
proof
defpred S1[ Element of T, set ] means ( ( Rainbow ($1,R) = {} implies $2 = 0 ) & ( for S being non empty Subset of ExtREAL st S = Rainbow ($1,R) holds
$2 = sup S ) );
A1: for x being Element of T ex y being Element of R^1 st S1[x,y]
proof
let x be Element of T; ::_thesis: ex y being Element of R^1 st S1[x,y]
percases ( Rainbow (x,R) = {} or Rainbow (x,R) <> {} ) ;
supposeA2: Rainbow (x,R) = {} ; ::_thesis: ex y being Element of R^1 st S1[x,y]
reconsider y = 0 as Element of R^1 by TOPMETR:17;
 S1[x,y] by A2;
hence  ex y being Element of R^1 st S1[x,y] ; ::_thesis: verum
end;
suppose Rainbow (x,R) <> {} ; ::_thesis: ex y being Element of R^1 st S1[x,y]
then reconsider S = Rainbow (x,R) as non empty Subset of ExtREAL ;
reconsider e1 = 1 as R_eal by XXREAL_0:def_1;
consider q being set  such that
A3: q in S by XBOOLE_0:def_1;
reconsider q = q as R_eal by A3;
 S c= DYADIC by Th13;
then  S c= [.0.,e1.] by URYSOHN2:28, XBOOLE_1:1;
then A4: ( 0 <= inf S & sup S <= e1 ) by URYSOHN2:26;
 ( inf S <= q & q <= sup S ) by A3, XXREAL_2:3, XXREAL_2:4;
then reconsider y = sup S as Element of R^1 by A4, TOPMETR:17, XXREAL_0:45;
take  y ; ::_thesis: S1[x,y]
thus  S1[x,y] ; ::_thesis: verum
end;
end;
end;
 ex F being Function of the carrier of T, the carrier of R^1 st
for x being Element of T holds S1[x,F . x] from FUNCT_2:sch_3(A1);
then consider F being Function of T,R^1 such that
A5: for x being Element of T holds S1[x,F . x] ;
take  F ; ::_thesis: for p being Point of T holds
( ( Rainbow (p,R) = {} implies F . p = 0 ) & ( for S being non empty Subset of ExtREAL st S = Rainbow (p,R) holds
F . p = sup S ) )
thus  for p being Point of T holds
( ( Rainbow (p,R) = {} implies F . p = 0 ) & ( for S being non empty Subset of ExtREAL st S = Rainbow (p,R) holds
F . p = sup S ) ) by A5; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Function of T,R^1 st ( for p being Point of T holds
( ( Rainbow (p,R) = {} implies b1 . p = 0 ) & ( for S being non empty Subset of ExtREAL st S = Rainbow (p,R) holds
b1 . p = sup S ) ) ) & ( for p being Point of T holds
( ( Rainbow (p,R) = {} implies b2 . p = 0 ) & ( for S being non empty Subset of ExtREAL st S = Rainbow (p,R) holds
b2 . p = sup S ) ) ) holds
b1 = b2
proof
let G1, G2 be Function of T,R^1; ::_thesis: ( ( for p being Point of T holds
( ( Rainbow (p,R) = {} implies G1 . p = 0 ) & ( for S being non empty Subset of ExtREAL st S = Rainbow (p,R) holds
G1 . p = sup S ) ) ) & ( for p being Point of T holds
( ( Rainbow (p,R) = {} implies G2 . p = 0 ) & ( for S being non empty Subset of ExtREAL st S = Rainbow (p,R) holds
G2 . p = sup S ) ) ) implies G1 = G2 )
assume that
A6: for p being Point of T holds
( ( Rainbow (p,R) = {} implies G1 . p = 0 ) & ( for S being non empty Subset of ExtREAL st S = Rainbow (p,R) holds
G1 . p = sup S ) ) and
A7: for p being Point of T holds
( ( Rainbow (p,R) = {} implies G2 . p = 0 ) & ( for S being non empty Subset of ExtREAL st S = Rainbow (p,R) holds
G2 . p = sup S ) ) ; ::_thesis: G1 = G2
 for x being set st x in the carrier of T holds
G1 . x = G2 . x
proof
let x be set ; ::_thesis: ( x in the carrier of T implies G1 . x = G2 . x )
assume  x in the carrier of T ; ::_thesis: G1 . x = G2 . x
then reconsider x = x as Point of T ;
percases ( Rainbow (x,R) = {} or Rainbow (x,R) <> {} ) ;
supposeA8: Rainbow (x,R) = {} ; ::_thesis: G1 . x = G2 . x
then G1 . x = 0 by A6
.= G2 . x by A7, A8 ;
hence  G1 . x = G2 . x ; ::_thesis: verum
end;
suppose Rainbow (x,R) <> {} ; ::_thesis: G1 . x = G2 . x
then reconsider S = Rainbow (x,R) as non empty Subset of ExtREAL ;
G1 . x = sup S by A6
.= G2 . x by A7 ;
hence  G1 . x = G2 . x ; ::_thesis: verum
end;
end;
end;
hence  G1 = G2 by FUNCT_2:12; ::_thesis: verum
end;
end;

:: deftheorem Def6 defines Thunder URYSOHN3:def_6_:_
 for T being non empty TopSpace
for A, B being Subset of T
for R being Rain of A,B
for b5 being Function of T,R^1 holds
( b5 = Thunder R iff for p being Point of T holds
( ( Rainbow (p,R) = {} implies b5 . p = 0 ) & ( for S being non empty Subset of ExtREAL st S = Rainbow (p,R) holds
b5 . p = sup S ) ) );

theorem Th14: :: URYSOHN3:14
for T being non empty TopSpace
for A, B being Subset of T
for G being Rain of A,B
for p being Point of T
for S being non empty Subset of ExtREAL st S = Rainbow (p,G) holds
for e1 being R_eal st e1 = 1 holds
( 0. <= sup S & sup S <= e1 )
proof
reconsider a = 0 , b = 1 as R_eal by XXREAL_0:def_1;
let T be non empty TopSpace; ::_thesis: for A, B being Subset of T
for G being Rain of A,B
for p being Point of T
for S being non empty Subset of ExtREAL st S = Rainbow (p,G) holds
for e1 being R_eal st e1 = 1 holds
( 0. <= sup S & sup S <= e1 )
let A, B be Subset of T; ::_thesis: for G being Rain of A,B
for p being Point of T
for S being non empty Subset of ExtREAL st S = Rainbow (p,G) holds
for e1 being R_eal st e1 = 1 holds
( 0. <= sup S & sup S <= e1 )
let G be Rain of A,B; ::_thesis: for p being Point of T
for S being non empty Subset of ExtREAL st S = Rainbow (p,G) holds
for e1 being R_eal st e1 = 1 holds
( 0. <= sup S & sup S <= e1 )
let p be Point of T; ::_thesis: for S being non empty Subset of ExtREAL st S = Rainbow (p,G) holds
for e1 being R_eal st e1 = 1 holds
( 0. <= sup S & sup S <= e1 )
let S be non empty Subset of ExtREAL; ::_thesis: ( S = Rainbow (p,G) implies for e1 being R_eal st e1 = 1 holds
( 0. <= sup S & sup S <= e1 ) )
consider s being set  such that
A1: s in S by XBOOLE_0:def_1;
reconsider s = s as R_eal by A1;
assume  S = Rainbow (p,G) ; ::_thesis: for e1 being R_eal st e1 = 1 holds
( 0. <= sup S & sup S <= e1 )
then  S c= DYADIC by Th13;
then A2: S c= [.a,b.] by URYSOHN2:28, XBOOLE_1:1;
let e1 be R_eal; ::_thesis: ( e1 = 1 implies ( 0. <= sup S & sup S <= e1 ) )
assume  e1 = 1 ; ::_thesis: ( 0. <= sup S & sup S <= e1 )
then  for x being ext-real number st x in S holds
x <= e1 by A2, XXREAL_1:1;
then A3: e1 is UpperBound of S by XXREAL_2:def_1;
 0. <= s by A2, A1, XXREAL_1:1;
hence  ( 0. <= sup S & sup S <= e1 ) by A3, A1, XXREAL_2:4, XXREAL_2:def_3; ::_thesis: verum
end;

theorem Th15: :: URYSOHN3:15
for T being non empty normal TopSpace
for A, B being closed Subset of T st A <> {} & A misses B holds
for G being Rain of A,B
for r being Element of DOM
for p being Point of T st (Thunder G) . p < r holds
p in (Tempest G) . r
proof
let T be non empty normal TopSpace; ::_thesis: for A, B being closed Subset of T st A <> {} & A misses B holds
for G being Rain of A,B
for r being Element of DOM
for p being Point of T st (Thunder G) . p < r holds
p in (Tempest G) . r
let A, B be closed Subset of T; ::_thesis: ( A <> {} & A misses B implies for G being Rain of A,B
for r being Element of DOM
for p being Point of T st (Thunder G) . p < r holds
p in (Tempest G) . r )
assume A1: ( A <> {} & A misses B ) ; ::_thesis: for G being Rain of A,B
for r being Element of DOM
for p being Point of T st (Thunder G) . p < r holds
p in (Tempest G) . r
let G be Rain of A,B; ::_thesis: for r being Element of DOM
for p being Point of T st (Thunder G) . p < r holds
p in (Tempest G) . r
let r be Element of DOM ; ::_thesis: for p being Point of T st (Thunder G) . p < r holds
p in (Tempest G) . r
let p be Point of T; ::_thesis: ( (Thunder G) . p < r implies p in (Tempest G) . r )
assume A2: (Thunder G) . p < r ; ::_thesis: p in (Tempest G) . r
now__::_thesis:_(_not_p_in_(Tempest_G)_._r_implies_p_in_(Tempest_G)_._r_)
percases ( Rainbow (p,G) = {} or Rainbow (p,G) <> {} ) ;
supposeA3: Rainbow (p,G) = {} ; ::_thesis: ( not p in (Tempest G) . r implies p in (Tempest G) . r )
assume A4: not p in (Tempest G) . r ; ::_thesis: p in (Tempest G) . r
 ( r in (halfline 0) \/ DYADIC or r in right_open_halfline 1 ) by URYSOHN1:def_3, XBOOLE_0:def_3;
then A5: ( r in halfline 0 or r in DYADIC or r in right_open_halfline 1 ) by XBOOLE_0:def_3;
A6: 0 < r by A2, A3, Def6;
now__::_thesis:_p_in_(Tempest_G)_._r
percases ( r in DYADIC or r in right_open_halfline 1 ) by A6, A5, XXREAL_1:233;
supposeA7: r in DYADIC ; ::_thesis: p in (Tempest G) . r
reconsider r1 = r as R_eal by XXREAL_0:def_1;
A8: for s being Real st s = r1 holds
not p in (Tempest G) . s by A4;
then reconsider S = Rainbow (p,G) as non empty Subset of ExtREAL by A7, Def5;
A9: (Thunder G) . p = sup S by Def6;
 r1 in Rainbow (p,G) by A7, A8, Def5;
hence  p in (Tempest G) . r by A2, A9, XXREAL_2:4; ::_thesis: verum
end;
suppose r in right_open_halfline 1 ; ::_thesis: p in (Tempest G) . r
then  (Tempest G) . r = the carrier of T by A1, Def4;
hence  p in (Tempest G) . r ; ::_thesis: verum
end;
end;
end;
hence  p in (Tempest G) . r ; ::_thesis: verum
end;
suppose Rainbow (p,G) <> {} ; ::_thesis: ( not p in (Tempest G) . r implies p in (Tempest G) . r )
then reconsider S = Rainbow (p,G) as non empty Subset of ExtREAL ;
reconsider e1 = 1 as R_eal by XXREAL_0:def_1;
consider s being set  such that
A10: s in S by XBOOLE_0:def_1;
reconsider s = s as R_eal by A10;
A11: s <= sup S by A10, XXREAL_2:4;
assume A12: not p in (Tempest G) . r ; ::_thesis: p in (Tempest G) . r
 ( r in (halfline 0) \/ DYADIC or r in right_open_halfline 1 ) by URYSOHN1:def_3, XBOOLE_0:def_3;
then A13: ( r in halfline 0 or r in DYADIC or r in right_open_halfline 1 ) by XBOOLE_0:def_3;
A14: (Thunder G) . p = sup S by Def6;
 for x being R_eal st x in S holds
( 0. <= x & x <= e1 )
proof
let x be R_eal; ::_thesis: ( x in S implies ( 0. <= x & x <= e1 ) )
assume  x in S ; ::_thesis: ( 0. <= x & x <= e1 )
then A15: x in DYADIC by Def5;
then reconsider x = x as Real ;
 ex n being Element of NAT st x in dyadic n by A15, URYSOHN1:def_2;
hence  ( 0. <= x & x <= e1 ) by URYSOHN1:1; ::_thesis: verum
end;
then A16: 0. <= s by A10;
now__::_thesis:_p_in_(Tempest_G)_._r
percases ( r in DYADIC or r in right_open_halfline 1 ) by A2, A14, A16, A11, A13, XXREAL_1:233;
supposeA17: r in DYADIC ; ::_thesis: p in (Tempest G) . r
reconsider r1 = r as R_eal by XXREAL_0:def_1;
 for s being Real st s = r1 holds
not p in (Tempest G) . s by A12;
then  r1 in Rainbow (p,G) by A17, Def5;
hence  p in (Tempest G) . r by A2, A14, XXREAL_2:4; ::_thesis: verum
end;
suppose r in right_open_halfline 1 ; ::_thesis: p in (Tempest G) . r
then  (Tempest G) . r = the carrier of T by A1, Def4;
hence  p in (Tempest G) . r ; ::_thesis: verum
end;
end;
end;
hence  p in (Tempest G) . r ; ::_thesis: verum
end;
end;
end;
hence  p in (Tempest G) . r ; ::_thesis: verum
end;

theorem Th16: :: URYSOHN3:16
for T being non empty normal TopSpace
for A, B being closed Subset of T st A <> {} & A misses B holds
for G being Rain of A,B
for r being Real st r in DYADIC \/ (right_open_halfline 1) & 0 < r holds
for p being Point of T st p in (Tempest G) . r holds
(Thunder G) . p <= r
proof
let T be non empty normal TopSpace; ::_thesis: for A, B being closed Subset of T st A <> {} & A misses B holds
for G being Rain of A,B
for r being Real st r in DYADIC \/ (right_open_halfline 1) & 0 < r holds
for p being Point of T st p in (Tempest G) . r holds
(Thunder G) . p <= r
let A, B be closed Subset of T; ::_thesis: ( A <> {} & A misses B implies for G being Rain of A,B
for r being Real st r in DYADIC \/ (right_open_halfline 1) & 0 < r holds
for p being Point of T st p in (Tempest G) . r holds
(Thunder G) . p <= r )
assume A1: ( A <> {} & A misses B ) ; ::_thesis: for G being Rain of A,B
for r being Real st r in DYADIC \/ (right_open_halfline 1) & 0 < r holds
for p being Point of T st p in (Tempest G) . r holds
(Thunder G) . p <= r
let G be Rain of A,B; ::_thesis: for r being Real st r in DYADIC \/ (right_open_halfline 1) & 0 < r holds
for p being Point of T st p in (Tempest G) . r holds
(Thunder G) . p <= r
let r be Real; ::_thesis: ( r in DYADIC \/ (right_open_halfline 1) & 0 < r implies for p being Point of T st p in (Tempest G) . r holds
(Thunder G) . p <= r )
assume that
A2: r in DYADIC \/ (right_open_halfline 1) and
A3: 0 < r ; ::_thesis: for p being Point of T st p in (Tempest G) . r holds
(Thunder G) . p <= r
let p be Point of T; ::_thesis: ( p in (Tempest G) . r implies (Thunder G) . p <= r )
assume A4: p in (Tempest G) . r ; ::_thesis: (Thunder G) . p <= r
percases ( r in DYADIC or r in right_open_halfline 1 ) by A2, XBOOLE_0:def_3;
supposeA5: r in DYADIC ; ::_thesis: (Thunder G) . p <= r
then  r in (halfline 0) \/ DYADIC by XBOOLE_0:def_3;
then A6: r in DOM by URYSOHN1:def_3, XBOOLE_0:def_3;
now__::_thesis:_(_(_Rainbow_(p,G)_=_{}_&_(Thunder_G)_._p_<=_r_)_or_(_Rainbow_(p,G)_<>_{}_&_(Thunder_G)_._p_<=_r_)_)
percases ( Rainbow (p,G) = {} or Rainbow (p,G) <> {} ) ;
case Rainbow (p,G) = {} ; ::_thesis: (Thunder G) . p <= r
hence  (Thunder G) . p <= r by A3, Def6; ::_thesis: verum
end;
case Rainbow (p,G) <> {} ; ::_thesis: (Thunder G) . p <= r
then reconsider S = Rainbow (p,G) as non empty Subset of ExtREAL ;
reconsider er = r as R_eal by XXREAL_0:def_1;
 for r1 being ext-real number st r1 in S holds
r1 <= er
proof
let r1 be ext-real number ; ::_thesis: ( r1 in S implies r1 <= er )
assume A7: r1 in S ; ::_thesis: r1 <= er
assume A8: not r1 <= er ; ::_thesis: contradiction
A9: S c= DYADIC by Th13;
then  r1 in DYADIC by A7;
then reconsider p1 = r1 as Real ;
percases ( inf_number_dyadic r <= inf_number_dyadic p1 or inf_number_dyadic p1 <= inf_number_dyadic r ) ;
supposeA10: inf_number_dyadic r <= inf_number_dyadic p1 ; ::_thesis: contradiction
set n = inf_number_dyadic p1;
 r in dyadic (inf_number_dyadic p1) by A5, A10, Th6;
then A11: (Tempest G) . r = (G . (inf_number_dyadic p1)) . r by A1, A5, A6, Def4;
reconsider D = G . (inf_number_dyadic p1) as Drizzle of A,B, inf_number_dyadic p1 by A1, Def2;
 p1 in (halfline 0) \/ DYADIC by A7, A9, XBOOLE_0:def_3;
then A12: p1 in DOM by URYSOHN1:def_3, XBOOLE_0:def_3;
 p1 in dyadic (inf_number_dyadic p1) by A7, A9, Th5;
then A13: (Tempest G) . p1 = (G . (inf_number_dyadic p1)) . p1 by A1, A7, A9, A12, Def4;
reconsider r = r, p1 = p1 as Element of dyadic (inf_number_dyadic p1) by A5, A7, A9, A10, Th6;
 ( Cl (D . r) c= D . p1 & D . r c= Cl (D . r) ) by A1, A8, Def1, PRE_TOPC:18;
then  D . r c= D . p1 by XBOOLE_1:1;
hence  contradiction by A4, A7, A11, A13, Def5; ::_thesis: verum
end;
suppose inf_number_dyadic p1 <= inf_number_dyadic r ; ::_thesis: contradiction
then A14: dyadic (inf_number_dyadic p1) c= dyadic (inf_number_dyadic r) by URYSOHN2:29;
set n = inf_number_dyadic r;
reconsider D = G . (inf_number_dyadic r) as Drizzle of A,B, inf_number_dyadic r by A1, Def2;
A15: p1 in dyadic (inf_number_dyadic p1) by A7, A9, Th5;
 p1 in (halfline 0) \/ DYADIC by A7, A9, XBOOLE_0:def_3;
then  p1 in DOM by URYSOHN1:def_3, XBOOLE_0:def_3;
then A16: (Tempest G) . p1 = (G . (inf_number_dyadic r)) . p1 by A1, A7, A9, A15, A14, Def4;
 r in dyadic (inf_number_dyadic r) by A5, Th6;
then A17: (Tempest G) . r = (G . (inf_number_dyadic r)) . r by A1, A5, A6, Def4;
reconsider p1 = p1 as Element of dyadic (inf_number_dyadic r) by A15, A14;
reconsider r = r as Element of dyadic (inf_number_dyadic r) by A5, Th6;
 ( Cl (D . r) c= D . p1 & D . r c= Cl (D . r) ) by A1, A8, Def1, PRE_TOPC:18;
then  D . r c= D . p1 by XBOOLE_1:1;
hence  contradiction by A4, A7, A17, A16, Def5; ::_thesis: verum
end;
end;
end;
then  r is UpperBound of S by XXREAL_2:def_1;
then  sup S <= er by XXREAL_2:def_3;
hence  (Thunder G) . p <= r by Def6; ::_thesis: verum
end;
end;
end;
hence  (Thunder G) . p <= r ; ::_thesis: verum
end;
suppose r in right_open_halfline 1 ; ::_thesis: (Thunder G) . p <= r
then A18: 1 < r by XXREAL_1:235;
now__::_thesis:_(_(_Rainbow_(p,G)_=_{}_&_(Thunder_G)_._p_<=_r_)_or_(_Rainbow_(p,G)_<>_{}_&_(Thunder_G)_._p_<=_r_)_)
percases ( Rainbow (p,G) = {} or Rainbow (p,G) <> {} ) ;
case Rainbow (p,G) = {} ; ::_thesis: (Thunder G) . p <= r
hence  (Thunder G) . p <= r by A18, Def6; ::_thesis: verum
end;
caseA19: Rainbow (p,G) <> {} ; ::_thesis: (Thunder G) . p <= r
reconsider e1 = 1 as R_eal by XXREAL_0:def_1;
consider S being non empty Subset of ExtREAL such that
A20: S = Rainbow (p,G) by A19;
 ( sup S <= e1 & (Thunder G) . p = sup S ) by A20, Def6, Th14;
hence  (Thunder G) . p <= r by A18, XXREAL_0:2; ::_thesis: verum
end;
end;
end;
hence  (Thunder G) . p <= r ; ::_thesis: verum
end;
end;
end;

theorem Th17: :: URYSOHN3:17
for T being non empty normal TopSpace
for A, B being closed Subset of T st A <> {} & A misses B holds
for G being Rain of A,B
for r1 being Element of DOM st 0 < r1 holds
for p being Point of T st r1 < (Thunder G) . p holds
not p in (Tempest G) . r1
proof
let T be non empty normal TopSpace; ::_thesis: for A, B being closed Subset of T st A <> {} & A misses B holds
for G being Rain of A,B
for r1 being Element of DOM st 0 < r1 holds
for p being Point of T st r1 < (Thunder G) . p holds
not p in (Tempest G) . r1
let A, B be closed Subset of T; ::_thesis: ( A <> {} & A misses B implies for G being Rain of A,B
for r1 being Element of DOM st 0 < r1 holds
for p being Point of T st r1 < (Thunder G) . p holds
not p in (Tempest G) . r1 )
assume A1: ( A <> {} & A misses B ) ; ::_thesis: for G being Rain of A,B
for r1 being Element of DOM st 0 < r1 holds
for p being Point of T st r1 < (Thunder G) . p holds
not p in (Tempest G) . r1
let G be Rain of A,B; ::_thesis: for r1 being Element of DOM st 0 < r1 holds
for p being Point of T st r1 < (Thunder G) . p holds
not p in (Tempest G) . r1
let r1 be Element of DOM ; ::_thesis: ( 0 < r1 implies for p being Point of T st r1 < (Thunder G) . p holds
not p in (Tempest G) . r1 )
assume A2: 0 < r1 ; ::_thesis: for p being Point of T st r1 < (Thunder G) . p holds
not p in (Tempest G) . r1
let p be Point of T; ::_thesis: ( r1 < (Thunder G) . p implies not p in (Tempest G) . r1 )
assume A3: ( r1 < (Thunder G) . p & p in (Tempest G) . r1 ) ; ::_thesis: contradiction
 ( r1 in (halfline 0) \/ DYADIC or r1 in right_open_halfline 1 ) by URYSOHN1:def_3, XBOOLE_0:def_3;
then  ( r1 in halfline 0 or r1 in DYADIC or r1 in right_open_halfline 1 ) by XBOOLE_0:def_3;
then  r1 in DYADIC \/ (right_open_halfline 1) by A2, XBOOLE_0:def_3, XXREAL_1:233;
hence  contradiction by A1, A2, A3, Th16; ::_thesis: verum
end;

theorem Th18: :: URYSOHN3:18
for T being non empty normal TopSpace
for A, B being closed Subset of T st A <> {} & A misses B holds
for G being Rain of A,B holds
( Thunder G is continuous & ( for x being Point of T holds
( 0 <= (Thunder G) . x & (Thunder G) . x <= 1 & ( x in A implies (Thunder G) . x = 0 ) & ( x in B implies (Thunder G) . x = 1 ) ) ) )
proof
A1: 1 in dyadic 0 by TARSKI:def_2, URYSOHN1:2;
then A2: 1 in DYADIC by URYSOHN1:def_2;
then  1 in (halfline 0) \/ DYADIC by XBOOLE_0:def_3;
then A3: 1 in DOM by URYSOHN1:def_3, XBOOLE_0:def_3;
reconsider e1 = 1 as R_eal by XXREAL_0:def_1;
let T be non empty normal TopSpace; ::_thesis: for A, B being closed Subset of T st A <> {} & A misses B holds
for G being Rain of A,B holds
( Thunder G is continuous & ( for x being Point of T holds
( 0 <= (Thunder G) . x & (Thunder G) . x <= 1 & ( x in A implies (Thunder G) . x = 0 ) & ( x in B implies (Thunder G) . x = 1 ) ) ) )
let A, B be closed Subset of T; ::_thesis: ( A <> {} & A misses B implies for G being Rain of A,B holds
( Thunder G is continuous & ( for x being Point of T holds
( 0 <= (Thunder G) . x & (Thunder G) . x <= 1 & ( x in A implies (Thunder G) . x = 0 ) & ( x in B implies (Thunder G) . x = 1 ) ) ) ) )
assume A4: ( A <> {} & A misses B ) ; ::_thesis: for G being Rain of A,B holds
( Thunder G is continuous & ( for x being Point of T holds
( 0 <= (Thunder G) . x & (Thunder G) . x <= 1 & ( x in A implies (Thunder G) . x = 0 ) & ( x in B implies (Thunder G) . x = 1 ) ) ) )
let G be Rain of A,B; ::_thesis: ( Thunder G is continuous & ( for x being Point of T holds
( 0 <= (Thunder G) . x & (Thunder G) . x <= 1 & ( x in A implies (Thunder G) . x = 0 ) & ( x in B implies (Thunder G) . x = 1 ) ) ) )
A5: 0 in dyadic 0 by TARSKI:def_2, URYSOHN1:2;
then A6: 0 in DYADIC by URYSOHN1:def_2;
then  0 in (halfline 0) \/ DYADIC by XBOOLE_0:def_3;
then A7: 0 in DOM by URYSOHN1:def_3, XBOOLE_0:def_3;
A8: for x being Point of T holds
( 0 <= (Thunder G) . x & (Thunder G) . x <= 1 & ( x in A implies (Thunder G) . x = 0 ) & ( x in B implies (Thunder G) . x = 1 ) )
proof
let x be Point of T; ::_thesis: ( 0 <= (Thunder G) . x & (Thunder G) . x <= 1 & ( x in A implies (Thunder G) . x = 0 ) & ( x in B implies (Thunder G) . x = 1 ) )
now__::_thesis:_(_(_Rainbow_(x,G)_=_{}_&_0_<=_(Thunder_G)_._x_&_(Thunder_G)_._x_<=_1_&_(_x_in_A_implies_(Thunder_G)_._x_=_0_)_&_(_x_in_B_implies_(Thunder_G)_._x_=_1_)_)_or_(_Rainbow_(x,G)_<>_{}_&_0_<=_(Thunder_G)_._x_&_(Thunder_G)_._x_<=_1_&_(_x_in_A_implies_(Thunder_G)_._x_=_0_)_&_(_x_in_B_implies_(Thunder_G)_._x_=_1_)_)_)
percases ( Rainbow (x,G) = {} or Rainbow (x,G) <> {} ) ;
caseA9: Rainbow (x,G) = {} ; ::_thesis: ( 0 <= (Thunder G) . x & (Thunder G) . x <= 1 & ( x in A implies (Thunder G) . x = 0 ) & ( x in B implies (Thunder G) . x = 1 ) )
 ( x in B implies (Thunder G) . x = 1 )
proof
 G . 0 is Drizzle of A,B, 0 by A4, Def2;
then A10: B = ([#] T) \ ((G . 0) . 1) by A4, Def1;
assume A11: x in B ; ::_thesis: (Thunder G) . x = 1
 (Tempest G) . 1 = (G . 0) . 1 by A4, A1, A2, A3, Def4;
then  for s being Real st s = 1 holds
not x in (Tempest G) . s by A11, A10, XBOOLE_0:def_5;
hence  (Thunder G) . x = 1 by A9, Def5, URYSOHN2:27; ::_thesis: verum
end;
hence  ( 0 <= (Thunder G) . x & (Thunder G) . x <= 1 & ( x in A implies (Thunder G) . x = 0 ) & ( x in B implies (Thunder G) . x = 1 ) ) by A9, Def6; ::_thesis: verum
end;
caseA12: Rainbow (x,G) <> {} ; ::_thesis: ( 0 <= (Thunder G) . x & (Thunder G) . x <= 1 & ( x in A implies (Thunder G) . x = 0 ) & ( x in B implies (Thunder G) . x = 1 ) )
A13: ( x in A implies (Thunder G) . x = 0 )
proof
assume A14: x in A ; ::_thesis: (Thunder G) . x = 0
A15: for s being R_eal st 0. < s holds
not s in Rainbow (x,G)
proof
let s be R_eal; ::_thesis: ( 0. < s implies not s in Rainbow (x,G) )
assume  0. < s ; ::_thesis: not s in Rainbow (x,G)
assume A16: s in Rainbow (x,G) ; ::_thesis: contradiction
then A17: s in DYADIC by Def5;
then reconsider s = s as Real ;
consider n being Element of NAT  such that
A18: s in dyadic n by A17, URYSOHN1:def_2;
 s in (halfline 0) \/ DYADIC by A17, XBOOLE_0:def_3;
then  s in DOM by URYSOHN1:def_3, XBOOLE_0:def_3;
then A19: (Tempest G) . s = (G . n) . s by A4, A17, A18, Def4;
reconsider r1 = 0 , r2 = s as Element of dyadic n by A18, URYSOHN1:6;
reconsider D = G . n as Drizzle of A,B,n by A4, Def2;
percases ( s = 0 or 0 < s ) by A18, URYSOHN1:1;
supposeA20: s = 0 ; ::_thesis: contradiction
 A c= D . 0 by A4, Def1;
hence  contradiction by A14, A16, A19, A20, Def5; ::_thesis: verum
end;
supposeA21: 0 < s ; ::_thesis: contradiction
A22: D . r1 c= Cl (D . r1) by PRE_TOPC:18;
 Cl (D . r1) c= D . r2 by A4, A21, Def1;
then A23: D . r1 c= D . r2 by A22, XBOOLE_1:1;
 A c= D . 0 by A4, Def1;
then  A c= D . s by A23, XBOOLE_1:1;
hence  contradiction by A14, A16, A19, Def5; ::_thesis: verum
end;
end;
end;
 G . 0 is Drizzle of A,B, 0 by A4, Def2;
then A24: A c= (G . 0) . 0 by A4, Def1;
A25: (Tempest G) . 0 = (G . 0) . 0 by A4, A5, A6, A7, Def4;
consider a being set  such that
A26: a in Rainbow (x,G) by A12, XBOOLE_0:def_1;
A27: a in DYADIC by A26, Def5;
then reconsider a = a as Real ;
A28: ex n being Element of NAT st a in dyadic n by A27, URYSOHN1:def_2;
percases ( a = 0 or 0 < a ) by A28, URYSOHN1:1;
suppose a = 0 ; ::_thesis: (Thunder G) . x = 0
hence  (Thunder G) . x = 0 by A14, A25, A24, A26, Def5; ::_thesis: verum
end;
suppose 0 < a ; ::_thesis: (Thunder G) . x = 0
hence  (Thunder G) . x = 0 by A15, A26; ::_thesis: verum
end;
end;
end;
reconsider S = Rainbow (x,G) as non empty Subset of ExtREAL by A12;
A29: sup S <= e1 by Th14;
A30: ( x in B implies (Thunder G) . x = 1 )
proof
 G . 0 is Drizzle of A,B, 0 by A4, Def2;
then A31: B = ([#] T) \ ((G . 0) . 1) by A4, Def1;
assume A32: x in B ; ::_thesis: (Thunder G) . x = 1
 (Tempest G) . 1 = (G . 0) . 1 by A4, A1, A2, A3, Def4;
then A33: for s being Real st s = 1 holds
not x in (Tempest G) . s by A32, A31, XBOOLE_0:def_5;
then reconsider S = Rainbow (x,G) as non empty Subset of ExtREAL by Def5, URYSOHN2:27;
 1 in Rainbow (x,G) by A33, Def5, URYSOHN2:27;
then A34: e1 <= sup S by XXREAL_2:4;
 (Thunder G) . x = sup S by Def6;
hence  (Thunder G) . x = 1 by A29, A34, XXREAL_0:1; ::_thesis: verum
end;
 ( e1 = 1 & (Thunder G) . x = sup S ) by Def6;
hence  ( 0 <= (Thunder G) . x & (Thunder G) . x <= 1 & ( x in A implies (Thunder G) . x = 0 ) & ( x in B implies (Thunder G) . x = 1 ) ) by A13, A30, Th14; ::_thesis: verum
end;
end;
end;
hence  ( 0 <= (Thunder G) . x & (Thunder G) . x <= 1 & ( x in A implies (Thunder G) . x = 0 ) & ( x in B implies (Thunder G) . x = 1 ) ) ; ::_thesis: verum
end;
 for p being Point of T holds Thunder G is_continuous_at p
proof
let p be Point of T; ::_thesis: Thunder G is_continuous_at p
 for Q being Subset of R^1 st Q is open & (Thunder G) . p in Q holds
ex H being Subset of T st
( H is open & p in H & (Thunder G) .: H c= Q )
proof
let Q be Subset of R^1; ::_thesis: ( Q is open & (Thunder G) . p in Q implies ex H being Subset of T st
( H is open & p in H & (Thunder G) .: H c= Q ) )
assume that
A35: Q is open and
A36: (Thunder G) . p in Q ; ::_thesis: ex H being Subset of T st
( H is open & p in H & (Thunder G) .: H c= Q )
reconsider x = (Thunder G) . p as Element of RealSpace by A36, TOPMETR:12, TOPMETR:def_6;
reconsider Q = Q as Subset of REAL by TOPMETR:17;
 ( the topology of R^1 = Family_open_set RealSpace & Q in the topology of R^1 ) by A35, PRE_TOPC:def_2, TOPMETR:12, TOPMETR:def_6;
then consider r being Real such that
A37: r > 0 and
A38: Ball (x,r) c= Q by A36, PCOMPS_1:def_4;
 ex r0 being Real st
( r0 < r & 0 < r0 & r0 <= 1 )
proof
percases ( r <= 1 or 1 < r ) ;
supposeA39: r <= 1 ; ::_thesis: ex r0 being Real st
( r0 < r & 0 < r0 & r0 <= 1 )
consider r0 being real number  such that
A40: ( 0 < r0 & r0 < r ) by A37, XREAL_1:5;
reconsider r0 = r0 as Real by XREAL_0:def_1;
take  r0 ; ::_thesis: ( r0 < r & 0 < r0 & r0 <= 1 )
thus  ( r0 < r & 0 < r0 & r0 <= 1 ) by A39, A40, XXREAL_0:2; ::_thesis: verum
end;
suppose 1 < r ; ::_thesis: ex r0 being Real st
( r0 < r & 0 < r0 & r0 <= 1 )
hence  ex r0 being Real st
( r0 < r & 0 < r0 & r0 <= 1 ) ; ::_thesis: verum
end;
end;
end;
then consider r0 being Real such that
A41: r0 < r and
A42: ( 0 < r0 & r0 <= 1 ) ;
consider r1 being Real such that
A43: r1 in DYADIC and
A44: 0 < r1 and
A45: r1 < r0 by A42, URYSOHN2:24;
A46: r1 in DYADIC \/ (right_open_halfline 1) by A43, XBOOLE_0:def_3;
consider n being Element of NAT  such that
A47: r1 in dyadic n by A43, URYSOHN1:def_2;
reconsider D = G . n as Drizzle of A,B,n by A4, Def2;
 r1 in (halfline 0) \/ DYADIC by A43, XBOOLE_0:def_3;
then A48: r1 in DOM by URYSOHN1:def_3, XBOOLE_0:def_3;
then A49: (Tempest G) . r1 = (G . n) . r1 by A4, A43, A47, Def4;
A50: r1 < r by A41, A45, XXREAL_0:2;
A51: for p being Point of T st p in (Tempest G) . r1 holds
(Thunder G) . p < r
proof
let p be Point of T; ::_thesis: ( p in (Tempest G) . r1 implies (Thunder G) . p < r )
assume  p in (Tempest G) . r1 ; ::_thesis: (Thunder G) . p < r
then  (Thunder G) . p <= r1 by A4, A44, A46, Th16;
hence  (Thunder G) . p < r by A50, XXREAL_0:2; ::_thesis: verum
end;
A52: the carrier of R^1 = the carrier of RealSpace by TOPMETR:12, TOPMETR:def_6;
reconsider r1 = r1 as Element of dyadic n by A47;
reconsider H = D . r1 as Subset of T ;
A53: 0 in dyadic n by URYSOHN1:6;
 ex H being Subset of T st
( H is open & p in H & (Thunder G) .: H c= Q )
proof
percases ( x = 0 or x <> 0 ) ;
supposeA54: x = 0 ; ::_thesis: ex H being Subset of T st
( H is open & p in H & (Thunder G) .: H c= Q )
take  H ; ::_thesis: ( H is open & p in H & (Thunder G) .: H c= Q )
 (Thunder G) .: H c= Q
proof
reconsider p = x as Real ;
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in (Thunder G) .: H or y in Q )
assume  y in (Thunder G) .: H ; ::_thesis: y in Q
then consider x1 being set  such that
 x1 in dom (Thunder G) and
A55: x1 in H and
A56: y = (Thunder G) . x1 by FUNCT_1:def_6;
reconsider y = y as Point of RealSpace by A52, A55, A56, FUNCT_2:5;
reconsider q = y as Real by METRIC_1:def_13;
A57: - (p - q) < r by A51, A49, A54, A55, A56;
reconsider x1 = x1 as Point of T by A55;
A58: 0 <= (Thunder G) . x1 by A8;
A59: q - p < r - 0 by A51, A49, A54, A55, A56;
then  p - q < r by A54, A56, A58, XREAL_1:14;
then A60: abs (p - q) <> r by A57, ABSVALUE:def_1;
A61: ( dist (x,y) < r implies y in Ball (x,r) ) by METRIC_1:11;
 - (- (p - q)) = p - q ;
then  - r < p - q by A57, XREAL_1:24;
then  ( dist (x,y) = abs (p - q) & abs (p - q) <= r ) by A54, A56, A58, A59, ABSVALUE:5, TOPMETR:11;
hence  y in Q by A38, A61, A60, XXREAL_0:1; ::_thesis: verum
end;
hence  ( H is open & p in H & (Thunder G) .: H c= Q ) by A4, A44, A48, A49, A53, A54, Def1, Th15; ::_thesis: verum
end;
supposeA62: x <> 0 ; ::_thesis: ex H being Subset of T st
( H is open & p in H & (Thunder G) .: H c= Q )
reconsider x = x as Real ;
 0 <= (Thunder G) . p by A8;
then consider r1, r2 being Real such that
A63: r1 in DYADIC \/ (right_open_halfline 1) and
 r2 in DYADIC \/ (right_open_halfline 1) and
A64: 0 < r1 and
A65: r1 < x and
A66: x < r2 and
A67: r2 - r1 < r by A37, A62, URYSOHN2:31;
 ( r1 in DYADIC or r1 in right_open_halfline 1 ) by A63, XBOOLE_0:def_3;
then  ( r1 in (halfline 0) \/ DYADIC or r1 in right_open_halfline 1 ) by XBOOLE_0:def_3;
then A68: r1 in DOM by URYSOHN1:def_3, XBOOLE_0:def_3;
then reconsider B = (Tempest G) . r1 as Subset of T by FUNCT_2:5;
reconsider C = ([#] T) \ (Cl B) as Subset of T ;
consider r3 being Real such that
A69: r3 in DOM and
A70: x < r3 and
A71: r3 < r2 by A66, URYSOHN2:25;
 Cl (Cl B) = Cl B ;
then  Cl B is closed by PRE_TOPC:22;
then A72: C is open by PRE_TOPC:def_3;
reconsider A = (Tempest G) . r3 as Subset of T by A69, FUNCT_2:5;
take H = A /\ C; ::_thesis: ( H is open & p in H & (Thunder G) .: H c= Q )
A73: (Thunder G) .: H c= Q
proof
reconsider x = x as Element of RealSpace ;
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in (Thunder G) .: H or y in Q )
reconsider p = x as Real ;
assume  y in (Thunder G) .: H ; ::_thesis: y in Q
then consider x1 being set  such that
 x1 in dom (Thunder G) and
A74: x1 in H and
A75: y = (Thunder G) . x1 by FUNCT_1:def_6;
reconsider x1 = x1 as Point of T by A74;
A76: x1 in (Tempest G) . r3 by A74, XBOOLE_0:def_4;
reconsider y = y as Real by A75;
reconsider y = y as Point of RealSpace by A52, A74, A75, FUNCT_2:5;
reconsider q = y as Real ;
A77: - (- (p - q)) = p - q ;
A78: not r3 <= 0 by A8, A70;
 ( r3 in (halfline 0) \/ DYADIC or r3 in right_open_halfline 1 ) by A69, URYSOHN1:def_3, XBOOLE_0:def_3;
then  ( r3 in halfline 0 or r3 in DYADIC or r3 in right_open_halfline 1 ) by XBOOLE_0:def_3;
then  r3 in DYADIC \/ (right_open_halfline 1) by A78, XBOOLE_0:def_3, XXREAL_1:233;
then  (Thunder G) . x1 <= r3 by A4, A76, A78, Th16;
then  (Thunder G) . x1 < r2 by A71, XXREAL_0:2;
then A79: q - p < r2 - r1 by A65, A75, XREAL_1:14;
then  - (p - q) < r by A67, XXREAL_0:2;
then A80: - r < p - q by A77, XREAL_1:24;
A81: x1 in ([#] T) \ (Cl B) by A74, XBOOLE_0:def_4;
 not x1 in B
proof
A82: B c= Cl B by PRE_TOPC:18;
assume  x1 in B ; ::_thesis: contradiction
hence  contradiction by A81, A82, XBOOLE_0:def_5; ::_thesis: verum
end;
then A83: p - q < r2 - r1 by A4, A66, A68, A75, Th15, XREAL_1:14;
then  p - q < r by A67, XXREAL_0:2;
then A84: ( dist (x,y) = abs (p - q) & abs (p - q) <= r ) by A80, ABSVALUE:5, TOPMETR:11;
A85: abs (p - q) <> r
proof
assume A86: abs (p - q) = r ; ::_thesis: contradiction
percases ( 0 <= p - q or p - q < 0 ) ;
suppose 0 <= p - q ; ::_thesis: contradiction
hence  contradiction by A67, A83, A86, ABSVALUE:def_1; ::_thesis: verum
end;
suppose p - q < 0 ; ::_thesis: contradiction
then  abs (p - q) = - (p - q) by ABSVALUE:def_1;
hence  contradiction by A67, A79, A86; ::_thesis: verum
end;
end;
end;
 ( dist (x,y) < r implies y in Ball (x,r) ) by METRIC_1:11;
hence  y in Q by A38, A84, A85, XXREAL_0:1; ::_thesis: verum
end;
 (Thunder G) . p <= 1 by A8;
then consider r4 being Real such that
A87: r4 in DYADIC and
A88: r1 < r4 and
A89: r4 < x by A64, A65, URYSOHN2:24;
A90: r4 in (halfline 0) \/ DYADIC by A87, XBOOLE_0:def_3;
then  r4 in DOM by URYSOHN1:def_3, XBOOLE_0:def_3;
then A91: Cl B c= (Tempest G) . r4 by A4, A88, A68, Th12;
reconsider r4 = r4 as Element of DOM by A90, URYSOHN1:def_3, XBOOLE_0:def_3;
 not p in (Tempest G) . r4 by A4, A64, A88, A89, Th17;
then  not p in Cl B by A91;
then A92: p in C by XBOOLE_0:def_5;
 ( A is open & p in (Tempest G) . r3 ) by A4, A69, A70, Th11, Th15;
hence  ( H is open & p in H & (Thunder G) .: H c= Q ) by A72, A92, A73, TOPS_1:11, XBOOLE_0:def_4; ::_thesis: verum
end;
end;
end;
hence  ex H being Subset of T st
( H is open & p in H & (Thunder G) .: H c= Q ) ; ::_thesis: verum
end;
hence  Thunder G is_continuous_at p by TMAP_1:43; ::_thesis: verum
end;
hence  ( Thunder G is continuous & ( for x being Point of T holds
( 0 <= (Thunder G) . x & (Thunder G) . x <= 1 & ( x in A implies (Thunder G) . x = 0 ) & ( x in B implies (Thunder G) . x = 1 ) ) ) ) by A8, TMAP_1:44; ::_thesis: verum
end;

theorem Th19: :: URYSOHN3:19
for T being non empty normal TopSpace
for A, B being closed Subset of T st A <> {} & A misses B holds
ex F being Function of T,R^1 st
( F is continuous & ( for x being Point of T holds
( 0 <= F . x & F . x <= 1 & ( x in A implies F . x = 0 ) & ( x in B implies F . x = 1 ) ) ) )
proof
let T be non empty normal TopSpace; ::_thesis: for A, B being closed Subset of T st A <> {} & A misses B holds
ex F being Function of T,R^1 st
( F is continuous & ( for x being Point of T holds
( 0 <= F . x & F . x <= 1 & ( x in A implies F . x = 0 ) & ( x in B implies F . x = 1 ) ) ) )
let A, B be closed Subset of T; ::_thesis: ( A <> {} & A misses B implies ex F being Function of T,R^1 st
( F is continuous & ( for x being Point of T holds
( 0 <= F . x & F . x <= 1 & ( x in A implies F . x = 0 ) & ( x in B implies F . x = 1 ) ) ) ) )
assume A1: ( A <> {} & A misses B ) ; ::_thesis: ex F being Function of T,R^1 st
( F is continuous & ( for x being Point of T holds
( 0 <= F . x & F . x <= 1 & ( x in A implies F . x = 0 ) & ( x in B implies F . x = 1 ) ) ) )
set R = the Rain of A,B;
take  Thunder the Rain of A,B ; ::_thesis: ( Thunder the Rain of A,B is continuous & ( for x being Point of T holds
( 0 <= (Thunder the Rain of A,B) . x & (Thunder the Rain of A,B) . x <= 1 & ( x in A implies (Thunder the Rain of A,B) . x = 0 ) & ( x in B implies (Thunder the Rain of A,B) . x = 1 ) ) ) )
thus  ( Thunder the Rain of A,B is continuous & ( for x being Point of T holds
( 0 <= (Thunder the Rain of A,B) . x & (Thunder the Rain of A,B) . x <= 1 & ( x in A implies (Thunder the Rain of A,B) . x = 0 ) & ( x in B implies (Thunder the Rain of A,B) . x = 1 ) ) ) ) by A1, Th18; ::_thesis: verum
end;

theorem Th20: :: URYSOHN3:20
for T being non empty normal TopSpace
for A, B being closed Subset of T st A misses B holds
ex F being Function of T,R^1 st
( F is continuous & ( for x being Point of T holds
( 0 <= F . x & F . x <= 1 & ( x in A implies F . x = 0 ) & ( x in B implies F . x = 1 ) ) ) )
proof
let T be non empty normal TopSpace; ::_thesis: for A, B being closed Subset of T st A misses B holds
ex F being Function of T,R^1 st
( F is continuous & ( for x being Point of T holds
( 0 <= F . x & F . x <= 1 & ( x in A implies F . x = 0 ) & ( x in B implies F . x = 1 ) ) ) )
let A, B be closed Subset of T; ::_thesis: ( A misses B implies ex F being Function of T,R^1 st
( F is continuous & ( for x being Point of T holds
( 0 <= F . x & F . x <= 1 & ( x in A implies F . x = 0 ) & ( x in B implies F . x = 1 ) ) ) ) )
assume A1: A misses B ; ::_thesis: ex F being Function of T,R^1 st
( F is continuous & ( for x being Point of T holds
( 0 <= F . x & F . x <= 1 & ( x in A implies F . x = 0 ) & ( x in B implies F . x = 1 ) ) ) )
percases ( A <> {} or A = {} ) ;
suppose A <> {} ; ::_thesis: ex F being Function of T,R^1 st
( F is continuous & ( for x being Point of T holds
( 0 <= F . x & F . x <= 1 & ( x in A implies F . x = 0 ) & ( x in B implies F . x = 1 ) ) ) )
hence  ex F being Function of T,R^1 st
( F is continuous & ( for x being Point of T holds
( 0 <= F . x & F . x <= 1 & ( x in A implies F . x = 0 ) & ( x in B implies F . x = 1 ) ) ) ) by A1, Th19; ::_thesis: verum
end;
supposeA2: A = {} ; ::_thesis: ex F being Function of T,R^1 st
( F is continuous & ( for x being Point of T holds
( 0 <= F . x & F . x <= 1 & ( x in A implies F . x = 0 ) & ( x in B implies F . x = 1 ) ) ) )
set S = the carrier of T;
set L = the carrier of R^1;
reconsider r = 1 as Element of the carrier of R^1 by TOPMETR:17;
defpred S1[ set , set ] means $2 = r;
A3: for x being Element of the carrier of T ex y being Element of the carrier of R^1 st S1[x,y] ;
 ex F being Function of the carrier of T, the carrier of R^1 st
for x being Element of the carrier of T holds S1[x,F . x] from FUNCT_2:sch_3(A3);
then consider F being Function of the carrier of T, the carrier of R^1 such that
A4: for x being Element of the carrier of T holds F . x = r ;
take  F ; ::_thesis: ( F is continuous & ( for x being Point of T holds
( 0 <= F . x & F . x <= 1 & ( x in A implies F . x = 0 ) & ( x in B implies F . x = 1 ) ) ) )
A5: dom F = the carrier of T by FUNCT_2:def_1;
thus  F is continuous ::_thesis: for x being Point of T holds
( 0 <= F . x & F . x <= 1 & ( x in A implies F . x = 0 ) & ( x in B implies F . x = 1 ) )
proof
 the carrier of T c= the carrier of T ;
then reconsider O1 = the carrier of T as Subset of T ;
reconsider O2 = {} as Subset of T by XBOOLE_1:2;
let P be Subset of R^1; :: according to PRE_TOPC:def_6 ::_thesis: ( not P is closed or K447( the carrier of T, the carrier of R^1,F,P) is closed )
assume  P is closed ; ::_thesis: K447( the carrier of T, the carrier of R^1,F,P) is closed
A6: O2 = ([#] T) \ O1 by XBOOLE_1:37;
A7: O2 is closed ;
percases ( 1 in P or not 1 in P ) ;
suppose 1 in P ; ::_thesis: K447( the carrier of T, the carrier of R^1,F,P) is closed
then  for x being set holds
( x in the carrier of T iff ( x in dom F & F . x in P ) ) by A4, FUNCT_2:def_1;
hence  K447( the carrier of T, the carrier of R^1,F,P) is closed by A6, FUNCT_1:def_7; ::_thesis: verum
end;
suppose not 1 in P ; ::_thesis: K447( the carrier of T, the carrier of R^1,F,P) is closed
then  for x being set holds
( x in {} iff ( x in dom F & F . x in P ) ) by A4, A5;
hence  K447( the carrier of T, the carrier of R^1,F,P) is closed by A7, FUNCT_1:def_7; ::_thesis: verum
end;
end;
end;
let x be Point of T; ::_thesis: ( 0 <= F . x & F . x <= 1 & ( x in A implies F . x = 0 ) & ( x in B implies F . x = 1 ) )
thus  ( 0 <= F . x & F . x <= 1 & ( x in A implies F . x = 0 ) & ( x in B implies F . x = 1 ) ) by A2, A4; ::_thesis: verum
end;
end;
end;

theorem :: URYSOHN3:21
for T being non empty T_2 compact TopSpace
for A, B being closed Subset of T st A misses B holds
ex F being Function of T,R^1 st
( F is continuous & ( for x being Point of T holds
( 0 <= F . x & F . x <= 1 & ( x in A implies F . x = 0 ) & ( x in B implies F . x = 1 ) ) ) ) by Th20;