urysohn3.miz



    begin

    

     Lm1: for T be non empty normal TopSpace, A,B be closed Subset of T st A <> {} & A misses B holds ex G be Function of ( dyadic 0 ), ( bool the carrier of T) st A c= (G . 0 ) & B = (( [#] T) \ (G . 1)) & for r1,r2 be 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;

      let A,B be closed Subset of T;

      assume that

       A1: A <> {} and

       A2: A misses B;

      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 be 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 P[ set, set] means ($1 = 0 implies $2 = G0) & ($1 = 1 implies $2 = G1);

      

       A8: for x be Element of ( dyadic 0 ) holds ex y be Subset of T st P[x, y]

      proof

        let x be Element of ( dyadic 0 );

        per cases by TARSKI:def 2, URYSOHN1: 2;

          suppose

           A9: x = 0 ;

          take G0;

          thus thesis by A9;

        end;

          suppose

           A10: x = 1;

          take G1;

          thus thesis by A10;

        end;

      end;

      ex F be Function of ( dyadic 0 ), ( bool the carrier of T) st for x be Element of ( dyadic 0 ) holds P[x, (F . x)] from FUNCT_2:sch 3( A8);

      then

      consider F be Function of ( dyadic 0 ), ( bool the carrier of T) such that

       A11: for x be Element of ( dyadic 0 ) holds P[x, (F . x)];

      

       A12: for r1,r2 be 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 );

        

         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;

        then (F . 1) = G1 by A11, A14, URYSOHN1: 2;

        hence thesis by A3, A5, A7, A11, A15, A13, A14, TOPS_1: 3;

      end;

      take F;

      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 thesis by A6, A11, A12, PRE_TOPC: 3;

    end;

    theorem :: URYSOHN3:1

    

     Th1: for T be non empty normal TopSpace, A,B be closed Subset of T st A <> {} & A misses B holds for n be Nat holds ex G be Function of ( dyadic n), ( bool the carrier of T) st A c= (G . 0 ) & B = (( [#] T) \ (G . 1)) & for r1,r2 be 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;

      let A,B be closed Subset of T;

      assume that

       A1: A <> {} and

       A2: A misses B;

      defpred P[ Nat] means ex G be Function of ( dyadic $1), ( bool the carrier of T) st A c= (G . 0 ) & B = (( [#] T) \ (G . 1)) & (for r1,r2 be 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 be Nat st P[n] holds P[(n + 1)]

      proof

        let n be Nat;

        given G be Function of ( dyadic n), ( bool the carrier of T) such that

         A4: A c= (G . 0 ) & B = (( [#] T) \ (G . 1)) & for r1,r2 be Element of ( dyadic n) st r1 < r2 holds (G . r1) is open & (G . r2) is open & ( Cl (G . r1)) c= (G . r2);

        consider F be 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 be 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;

        thus thesis by A5;

      end;

      

       A6: P[ 0 ] by A1, A2, Lm1;

      thus for n be Nat holds P[n] from NAT_1:sch 2( A6, A3);

    end;

    definition

      let T be non empty TopSpace;

      let A,B be Subset of T;

      let n be Nat;

      assume

       A1: T is normal & A <> {} & A is closed & B is closed & A misses B;

      :: URYSOHN3:def1

      mode Drizzle of A,B,n -> Function of ( dyadic n), ( bool the carrier of T) means

      : Def1: A c= (it . 0 ) & B = (( [#] T) \ (it . 1)) & for r1,r2 be Element of ( dyadic n) st r1 < r2 holds (it . r1) is open & (it . r2) is open & ( Cl (it . r1)) c= (it . r2);

      existence by A1, Th1;

    end

    theorem :: URYSOHN3:2

    

     Th2: for T be non empty normal TopSpace, A,B be closed Subset of T st A <> {} & A misses B holds for n be Nat, G be Drizzle of A, B, n holds ex F be Drizzle of A, B, (n + 1) st for r be Element of ( dyadic (n + 1)) st r in ( dyadic n) holds (F . r) = (G . r)

    proof

      let T be non empty normal TopSpace;

      let A,B be closed Subset of T;

      assume that

       A1: A <> {} and

       A2: A misses B;

      let n be Nat;

      let G be Drizzle of A, B, n;

      

       A3: for r1,r2 be 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 be 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 be 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 be 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 as Drizzle of A, B, (n + 1) by A1, A2, A4, Def1;

      take F;

      let r be Element of ( dyadic (n + 1));

      

       A6: 0 in ( dyadic (n + 1)) & 1 in ( dyadic (n + 1)) by URYSOHN1: 6;

      assume r in ( dyadic n);

      hence thesis by A5, A6;

    end;

    theorem :: URYSOHN3:3

    

     Th3: for T be non empty TopSpace, A,B be Subset of T, n be Nat, S be Drizzle of A, B, n holds S is Element of ( PFuncs ( DYADIC ,( bool the carrier of T)))

    proof

      let T be non empty TopSpace;

      let A,B be Subset of T;

      let n be Nat;

      let S be Drizzle of A, B, n;

      ( dyadic n) c= DYADIC by URYSOHN2: 23;

      then S is PartFunc of DYADIC , ( bool the carrier of T) by RELSET_1: 7;

      hence thesis by PARTFUN1: 45;

    end;

    theorem :: URYSOHN3:4

    

     Th4: for T be non empty normal TopSpace, A,B be closed Subset of T st A <> {} & A misses B holds ex F be Functional_Sequence of DYADIC , ( bool the carrier of T) st for n be Nat holds (F . n) is Drizzle of A, B, n & for r be Element of ( dom (F . n)) holds ((F . n) . r) = ((F . (n + 1)) . r)

    proof

      let T be non empty normal TopSpace;

      let A,B be closed Subset of T;

      defpred P[ object] means ex n be Nat st $1 is Drizzle of A, B, n;

      consider D be set such that

       A1: for x be object holds x in D iff x in ( PFuncs ( DYADIC ,( bool the carrier of T))) & P[x] from XBOOLE_0:sch 1;

      set S = the Drizzle of A, B, 0 ;

      

       A2: S is Element of ( PFuncs ( DYADIC ,( bool the carrier of T))) by Th3;

      then

      reconsider D as non empty set by A1;

      reconsider S as Element of D by A1, A2;

      defpred P1[ Element of D, Element of D] means ex xx,yy be PartFunc of DYADIC , ( bool the carrier of T) st (xx = $1 & yy = $2 & (ex k be Nat st xx is Drizzle of A, B, k) & (for k be Nat st xx is Drizzle of A, B, k holds yy is Drizzle of A, B, (k + 1)) & (for r be Element of ( dom xx) holds (xx . r) = (yy . r)));

      defpred Q[ Nat, Element of D, Element of D] means P1[$2, $3];

      assume

       A3: A <> {} & A misses B;

      

       A4: for n be Nat holds for x be Element of D holds ex y be Element of D st Q[n, x, y]

      proof

        let n be Nat;

        let x be Element of D;

        consider s0 be 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 be Drizzle of A, B, (s0 + 1) such that

         A6: for r be Element of ( dyadic (s0 + 1)) holds (r in ( dyadic s0) implies (yy . r) = (xx . r)) by A3, Th2;

        

         A7: for r be Element of ( dom xx) holds (xx . r) = (yy . r)

        proof

          let r be Element of ( dom xx);

          ( 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 thesis by A6, A8;

        end;

        

         A9: for k be Nat st xx is Drizzle of A, B, k holds yy is Drizzle of A, B, (k + 1)

        proof

          let k be Nat;

          assume xx is Drizzle of A, B, k;

          then

           A10: ( dom xx) = ( dyadic k) by FUNCT_2:def 1;

          k = s0

          proof

            assume

             A11: k <> s0;

            per cases by A11, XXREAL_0: 1;

              suppose

               A12: k < s0;

              set o = (1 / (2 |^ s0));

              

               A13: not o in ( dyadic k)

              proof

                

                 A14: (2 |^ k) < (1 * (2 |^ s0)) by A12, PEPIN: 66;

                assume o in ( dyadic k);

                then

                consider i be Nat such that i <= (2 |^ k) and

                 A15: o = (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: not ex n be Nat st i = (n + 1)

                proof

                  given n be Nat such that

                   A20: i = (n + 1);

                  ((n + 1) - 1) < 0 by A18, A14, A20, XREAL_1: 49, XREAL_1: 83;

                  hence thesis;

                end;

                i <> 0 by A17, NEWTON: 83;

                hence thesis by A19, NAT_1: 6;

              end;

              1 <= (2 |^ s0) by PREPOWER: 11;

              then o in ( dyadic s0) by URYSOHN1:def 1;

              hence thesis by A10, A13, FUNCT_2:def 1;

            end;

              suppose

               A21: s0 < k;

              set o = (1 / (2 |^ k));

              

               A22: not o in ( dyadic s0)

              proof

                

                 A23: (2 |^ s0) < (1 * (2 |^ k)) by A21, PEPIN: 66;

                assume o in ( dyadic s0);

                then

                consider i be Nat such that i <= (2 |^ s0) and

                 A24: o = (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: not ex n be Nat st i = (n + 1)

                proof

                  given n be Nat such that

                   A29: i = (n + 1);

                  ((n + 1) - 1) < 0 by A27, A23, A29, XREAL_1: 49, XREAL_1: 83;

                  hence thesis;

                end;

                i <> 0 by A26, NEWTON: 83;

                hence thesis by A28, NAT_1: 6;

              end;

              1 <= (2 |^ k) by PREPOWER: 11;

              then o in ( dyadic k) by URYSOHN1:def 1;

              hence thesis by A10, A22, FUNCT_2:def 1;

            end;

          end;

          hence thesis;

        end;

        reconsider xx as Element of ( PFuncs ( DYADIC ,( bool the carrier of T))) by Th3;

        reconsider xx as Element of D;

        

         A30: yy is Element of ( PFuncs ( DYADIC ,( bool the carrier of T))) by Th3;

        then

        reconsider yy as Element of D by A1;

        ex y be Element of D st P1[x, y]

        proof

          take yy;

          reconsider yy as PartFunc of DYADIC , ( bool the carrier of T) by A30, PARTFUN1: 46;

          reconsider xx as PartFunc of DYADIC , ( bool the carrier of T) by PARTFUN1: 47;

          take xx, yy;

          thus thesis by A9, A7;

        end;

        then

        consider y be Element of D such that

         A31: P1[x, y];

        take y;

        thus thesis by A31;

      end;

      ex F be sequence of D st (F . 0 ) = S & for n be Nat holds Q[n, (F . n), (F . (n + 1))] from RECDEF_1:sch 2( A4);

      then

      consider F be sequence of D such that

       A32: (F . 0 ) = S and

       A33: for n be Nat holds P1[(F . n), (F . (n + 1))];

      for x be object holds x in D implies 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;

      then

       A34: ( dom F) = NAT & ( rng F) c= ( PFuncs ( DYADIC ,( bool the carrier of T))) by FUNCT_2:def 1;

      defpred R[ 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 be Nat st $2 is Drizzle of A, B, k) & (for k be Nat st $2 is Drizzle of A, B, k holds $3 is Drizzle of A, B, (k + 1)) & (for r be Element of ( dom $2) holds ($2 . r) = ($3 . r)));

      reconsider F as Functional_Sequence of DYADIC , ( bool the carrier of T) by A34, FUNCT_2:def 1, RELSET_1: 4;

      defpred P[ Nat] means (F . $1) is Drizzle of A, B, $1 & for r be Element of ( dom (F . $1)) holds ((F . $1) . r) = ((F . ($1 + 1)) . r);

      

       A35: for n be Nat st P[n] holds P[(n + 1)]

      proof

        let n be Nat;

        assume

         A36: P[n];

        ex xx,yy be PartFunc of DYADIC , ( bool the carrier of T) st R[n, xx, yy] by A33;

        hence (F . (n + 1)) is Drizzle of A, B, (n + 1) by A36;

        let r be Element of ( dom (F . (n + 1)));

        ex xx1,yy1 be PartFunc of DYADIC , ( bool the carrier of T) st R[(n + 1), xx1, yy1] by A33;

        hence thesis;

      end;

      take F;

      ex xx,yy be PartFunc of DYADIC , ( bool the carrier of T) st R[ 0 , xx, yy] by A33;

      then

       A37: P[ 0 ] by A32;

      for n be Nat holds P[n] from NAT_1:sch 2( A37, A35);

      hence thesis;

    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;

      :: URYSOHN3:def2

      mode Rain of A,B -> Functional_Sequence of DYADIC , ( bool the carrier of T) means

      : Def2: for n be Nat holds (it . n) is Drizzle of A, B, n & for r be Element of ( dom (it . n)) holds ((it . n) . r) = ((it . (n + 1)) . r);

      existence by A1, Th4;

    end

    definition

      let x be Real;

      assume

       A1: x in DYADIC ;

      :: URYSOHN3:def3

      func inf_number_dyadic (x) -> Nat means

      : Def3: (x in ( dyadic 0 ) iff it = 0 ) & for n be Nat st x in ( dyadic (n + 1)) & not x in ( dyadic n) holds it = (n + 1);

      existence

      proof

        defpred P[ Nat] means x in ( dyadic $1);

        ex s be Nat st P[s] by A1, URYSOHN1:def 2;

        then

         A2: ex s be Nat st P[s];

        ex q be Nat st P[q] & for i be Nat st P[i] holds q <= i from NAT_1:sch 5( A2);

        then

        consider q be Nat such that

         A3: x in ( dyadic q) and

         A4: for i be Nat st x in ( dyadic i) holds q <= i;

        reconsider q as Nat;

        take q;

        for n be Nat st x in ( dyadic (n + 1)) & not x in ( dyadic n) holds q = (n + 1)

        proof

          let n be Nat;

          assume that

           A5: x in ( dyadic (n + 1)) and

           A6: not x in ( dyadic n);

          

           A7: (n + 1) <= q

          proof

            assume not (n + 1) <= q;

            then q <= n by NAT_1: 13;

            then ( dyadic q) c= ( dyadic n) by URYSOHN2: 29;

            hence thesis by A3, A6;

          end;

          q <= (n + 1) by A4, A5;

          hence thesis by A7, XXREAL_0: 1;

        end;

        hence thesis by A3, A4;

      end;

      uniqueness

      proof

        let s1,s2 be Nat such that

         A8: x in ( dyadic 0 ) iff s1 = 0 and

         A9: for n be 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 be Nat st x in ( dyadic (n + 1)) & not x in ( dyadic n) holds s2 = (n + 1);

        per cases ;

          suppose s1 = 0 ;

          hence thesis by A8, A10;

        end;

          suppose

           A12: 0 < s1;

          defpred P[ Nat] means x in ( dyadic $1);

          ex s be Nat st P[s] by A1, URYSOHN1:def 2;

          then

           A13: ex s be Nat st P[s];

          ex q be Nat st P[q] & for i be Nat st P[i] holds q <= i from NAT_1:sch 5( A13);

          then

          consider q be Nat such that

           A14: x in ( dyadic q) and

           A15: for i be Nat st x in ( dyadic i) holds q <= i;

          now

            per cases ;

              case q = 0 ;

              hence thesis by A8, A12, A14;

            end;

              case 0 < q;

              then

              consider m be Nat such that

               A16: q = (m + 1) by NAT_1: 6;

              reconsider m as Nat;

              

               A17: not x in ( dyadic m)

              proof

                assume x in ( dyadic m);

                then (m + 1) <= (m + 0 ) by A15, A16;

                hence thesis by XREAL_1: 6;

              end;

              then s1 = (m + 1) by A9, A14, A16;

              hence thesis by A11, A14, A16, A17;

            end;

          end;

          hence thesis;

        end;

      end;

    end

    theorem :: URYSOHN3:5

    

     Th5: for x be Real st x in DYADIC holds x in ( dyadic ( inf_number_dyadic x))

    proof

      let x be Real;

      set s = ( inf_number_dyadic x);

      defpred P[ Nat] means not x in ( dyadic ((s + 1) + $1));

      assume

       A1: x in DYADIC ;

      then

      consider k be Nat such that

       A2: x in ( dyadic k) by URYSOHN1:def 2;

      

       A3: for i be Nat st P[i] holds P[(i + 1)]

      proof

        let i be Nat;

        assume

         A4: not x in ( dyadic ((s + 1) + i));

        assume x in ( dyadic ((s + 1) + (i + 1)));

        then x in ( dyadic (((s + 1) + i) + 1));

        then (s + 0 ) = (s + (i + 2)) by A1, A4, Def3;

        hence thesis;

      end;

      assume

       A5: not x in ( dyadic s);

      

       A6: s < k

      proof

        assume not s < k;

        then ( dyadic k) c= ( dyadic s) by URYSOHN2: 29;

        hence thesis by A5, A2;

      end;

      then

      consider i be Nat such that

       A7: k = (i + 1) by NAT_1: 6;

      s <= i by A6, A7, NAT_1: 13;

      then

      consider m be Nat such that

       A8: i = (s + m) by NAT_1: 10;

      reconsider m as Nat;

      

       A9: P[ 0 ] by A1, A5, Def3;

      for i be Nat holds P[i] from NAT_1:sch 2( A9, A3);

      then not x in ( dyadic ((s + 1) + m));

      hence thesis by A2, A7, A8;

    end;

    theorem :: URYSOHN3:6

    

     Th6: for x be Real st x in DYADIC holds for n be Nat st ( inf_number_dyadic x) <= n holds x in ( dyadic n)

    proof

      let x be Real;

      assume x in DYADIC ;

      then

       A1: x in ( dyadic ( inf_number_dyadic x)) by Th5;

      let n be Nat;

      assume ( inf_number_dyadic x) <= n;

      then ( dyadic ( inf_number_dyadic x)) c= ( dyadic n) by URYSOHN2: 29;

      hence thesis by A1;

    end;

    theorem :: URYSOHN3:7

    

     Th7: for x be Real, n be Nat st x in ( dyadic n) holds ( inf_number_dyadic x) <= n

    proof

      let x be Real;

      let n be Nat;

      

       A1: ( dyadic n) c= DYADIC by URYSOHN2: 23;

      defpred P[ Nat] means x in ( dyadic $1);

      assume

       A2: x in ( dyadic n);

      then

       A3: ex s be Nat st P[s];

      ex q be Nat st P[q] & for i be Nat st P[i] holds q <= i from NAT_1:sch 5( A3);

      then

      consider q be Nat such that

       A4: x in ( dyadic q) and

       A5: for i be Nat st x in ( dyadic i) holds q <= i;

      

       A6: q <= n by A2, A5;

      now

        per cases ;

          case q = 0 ;

          hence thesis by A2, A1, A4, Def3;

        end;

          case 0 < q;

          then

          consider m be Nat such that

           A7: q = (m + 1) by NAT_1: 6;

          reconsider m as Nat;

           not x in ( dyadic m)

          proof

            assume x in ( dyadic m);

            then (m + 1) <= (m + 0 ) by A5, A7;

            hence thesis by XREAL_1: 6;

          end;

          hence thesis by A2, A1, A4, A6, A7, Def3;

        end;

      end;

      hence thesis;

    end;

    theorem :: URYSOHN3:8

    

     Th8: for T be non empty normal TopSpace, A,B be closed Subset of T st A <> {} & A misses B holds for G be Rain of A, B, x be Real st x in DYADIC holds for n be Nat holds ((G . ( inf_number_dyadic x)) . x) = ((G . (( inf_number_dyadic x) + n)) . x)

    proof

      let T be non empty normal TopSpace;

      let A,B be closed Subset of T;

      assume

       A1: A <> {} & A misses B;

      let G be Rain of A, B;

      let x be Real;

      set s = ( inf_number_dyadic x);

      defpred Q[ Nat] means ((G . s) . x) = ((G . (s + $1)) . x);

      assume

       A2: x in DYADIC ;

      

       A3: for n be Nat st Q[n] holds Q[(n + 1)]

      proof

        let n be Nat;

        assume

         A4: ((G . s) . x) = ((G . (s + n)) . x);

        s <= (s + (n + 1)) by NAT_1: 11;

        then

         A5: x in ( dyadic ((s + n) + 1)) by A2, Th6;

        (G . (s + n)) is Drizzle of A, B, (s + n) by A1, Def2;

        then

         A6: ( dom (G . (s + n))) = ( dyadic (s + n)) by FUNCT_2:def 1;

        x in ( dyadic (s + n)) by A2, Th6, NAT_1: 11;

        hence thesis by A1, A4, A5, A6, Def2;

      end;

      

       A7: Q[ 0 ];

      for i be Nat holds Q[i] from NAT_1:sch 2( A7, A3);

      hence thesis;

    end;

    theorem :: URYSOHN3:9

    

     Th9: for T be non empty normal TopSpace, A,B be closed Subset of T st A <> {} & A misses B holds for G be Rain of A, B, x be Real st x in DYADIC holds ex y be Subset of T st for n be Nat st x in ( dyadic n) holds y = ((G . n) . x)

    proof

      let T be non empty normal TopSpace;

      let A,B be closed Subset of T;

      assume

       A1: A <> {} & A misses B;

      let G be Rain of A, B;

      let x be Real;

      assume

       A2: x in DYADIC ;

      reconsider s = ( inf_number_dyadic x) as 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;

      let n be Nat;

      assume x in ( dyadic n);

      then

      consider m be Nat such that

       A3: n = (s + m) by Th7, NAT_1: 10;

      thus thesis by A1, A2, A3, Th8;

    end;

    theorem :: URYSOHN3:10

    

     Th10: for T be non empty normal TopSpace, A,B be closed Subset of T st A <> {} & A misses B holds for G be Rain of A, B holds ex F be Function of DOM , ( bool the carrier of T) st for x be 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 be Nat st x in ( dyadic n) holds (F . x) = ((G . n) . x))

    proof

      let T be non empty normal TopSpace;

      let A,B be closed Subset of T;

      assume

       A1: A <> {} & A misses B;

      let G be Rain of A, B;

      defpred P[ 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 be Nat st $1 in ( dyadic n) holds $2 = ((G . n) . $1))));

      

       A2: for x be Element of DOM holds ex y be Subset of T st P[x, y]

      proof

        reconsider a = 0 , b = 1 as R_eal by XXREAL_0:def 1;

        let x be Element of DOM ;

        

         A3: x in (( halfline 0 ) \/ DYADIC ) or x in ( right_open_halfline 1) by URYSOHN1:def 3, XBOOLE_0:def 3;

        per cases by A3, XBOOLE_0:def 3;

          suppose

           A4: x in ( halfline 0 );

          

           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 ;

            per cases by A6;

              suppose x in ( right_open_halfline 1);

              then 1 < x by XXREAL_1: 235;

              hence thesis by A4, XXREAL_1: 233;

            end;

              suppose

               A7: x in DYADIC ;

              reconsider x as R_eal by XXREAL_0:def 1;

              a <= x by A7, URYSOHN2: 28, XXREAL_1: 1;

              hence thesis by A4, XXREAL_1: 233;

            end;

          end;

          reconsider s = {} as Subset of T by XBOOLE_1: 2;

          s = s;

          hence thesis by A5;

        end;

          suppose

           A8: x in DYADIC ;

          

           A9: not x in ( halfline 0 )

          proof

            assume

             A10: x in ( halfline 0 );

            reconsider x as R_eal by XXREAL_0:def 1;

            a <= x by A8, URYSOHN2: 28, XXREAL_1: 1;

            hence thesis by A10, XXREAL_1: 233;

          end;

          

           A11: not x in ( right_open_halfline 1)

          proof

            assume

             A12: x in ( right_open_halfline 1);

            reconsider x as R_eal by XXREAL_0:def 1;

            x <= b by A8, URYSOHN2: 28, XXREAL_1: 1;

            hence thesis by A12, XXREAL_1: 235;

          end;

          ex s be Subset of T st for n be Nat st x in ( dyadic n) holds s = ((G . n) . x) by A1, A8, Th9;

          hence thesis by A11, A9;

        end;

          suppose

           A13: x in ( right_open_halfline 1);

          

           A14: not x in ( halfline 0 ) & not x in DYADIC

          proof

            assume

             A15: x in ( halfline 0 ) or x in DYADIC ;

            per cases by A15;

              suppose x in ( halfline 0 );

              then x < 0 by XXREAL_1: 233;

              hence thesis by A13, XXREAL_1: 235;

            end;

              suppose

               A16: x in DYADIC ;

              reconsider x as R_eal by XXREAL_0:def 1;

              x <= b by A16, URYSOHN2: 28, XXREAL_1: 1;

              hence thesis by A13, XXREAL_1: 235;

            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 thesis by A14;

        end;

      end;

      ex F be Function of DOM , ( bool the carrier of T) st for x be Element of DOM holds P[x, (F . x)] from FUNCT_2:sch 3( A2);

      then

      consider F be Function of DOM , ( bool the carrier of T) such that

       A17: for x be Element of DOM holds P[x, (F . x)];

      take F;

      thus thesis by A17;

    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;

      :: URYSOHN3:def4

      func Tempest (R) -> Function of DOM , ( bool the carrier of T) means

      : Def4: for x be 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 be Nat st x in ( dyadic n) holds (it . x) = ((R . n) . x));

      existence by A1, Th10;

      uniqueness

      proof

        let G1,G2 be Function of DOM , ( bool the carrier of T) such that

         A2: for x be 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 be Nat st x in ( dyadic n) holds (G1 . x) = ((R . n) . x)) and

         A3: for x be 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 be Nat st x in ( dyadic n) holds (G2 . x) = ((R . n) . x));

        for x be object st x in DOM holds (G1 . x) = (G2 . x)

        proof

          let x be object;

          assume

           A4: x in DOM ;

          then

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

          per cases by A5, XBOOLE_0:def 3;

            suppose

             A6: x in ( halfline 0 );

            then (G1 . x) = {} by A2, A4;

            hence thesis by A3, A4, A6;

          end;

            suppose

             A7: x in ( right_open_halfline 1);

            then (G1 . x) = the carrier of T by A2, A4;

            hence thesis by A3, A4, A7;

          end;

            suppose

             A8: x in DYADIC ;

            then

            consider n be Nat such that

             A9: x in ( dyadic n) by URYSOHN1:def 2;

            (G1 . x) = ((R . n) . x) by A2, A4, A8, A9;

            hence thesis by A3, A4, A8, A9;

          end;

        end;

        hence thesis by FUNCT_2: 12;

      end;

    end

    theorem :: URYSOHN3:11

    

     Th11: for T be non empty normal TopSpace, A,B be closed Subset of T st A <> {} & A misses B holds for G be Rain of A, B, r be Real, C be Subset of T st C = (( Tempest G) . r) & r in DOM holds C is open

    proof

      let T be non empty normal TopSpace;

      let A,B be closed Subset of T;

      assume

       A1: A <> {} & A misses B;

      let G be Rain of A, B;

      let r be Real;

      let C be Subset of T;

      assume that

       A2: C = (( Tempest G) . r) and

       A3: r in DOM ;

      

       A4: r in (( halfline 0 ) \/ DYADIC ) or r in ( right_open_halfline 1) by A3, URYSOHN1:def 3, XBOOLE_0:def 3;

      per cases by A4, XBOOLE_0:def 3;

        suppose r in ( halfline 0 );

        then C = {} by A1, A2, A3, Def4;

        then C in the topology of T by PRE_TOPC: 1;

        hence thesis;

      end;

        suppose

         A5: r in DYADIC ;

        then

        consider n be 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 be 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

          per cases by A6, URYSOHN1: 1;

            case

             A9: r = 0 ;

            then

            reconsider 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 thesis by A1, A9, Def1;

          end;

            case

             A10: 0 < r;

             0 in ( dyadic n) by URYSOHN1: 6;

            hence thesis by A2, A6, A8, A7, A10;

          end;

        end;

        hence thesis;

      end;

        suppose

         A11: r in ( right_open_halfline 1);

        

         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 thesis by A12;

      end;

    end;

    theorem :: URYSOHN3:12

    

     Th12: for T be non empty normal TopSpace, A,B be closed Subset of T st A <> {} & A misses B holds for G be Rain of A, B holds for r1,r2 be Real st r1 in DOM & r2 in DOM & r1 < r2 holds for C be Subset of T st C = (( Tempest G) . r1) holds ( Cl C) c= (( Tempest G) . r2)

    proof

      let T be non empty normal TopSpace;

      let A,B be closed Subset of T;

      assume

       A1: A <> {} & A misses B;

      let G be Rain of A, B;

      let r1,r2 be Real;

      assume that

       A2: r1 in DOM and

       A3: r2 in DOM and

       A4: r1 < 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;

      assume

       A7: C = (( Tempest G) . r1);

      per cases by A5, A6, XBOOLE_0:def 3;

        suppose

         A8: r1 in ( halfline 0 ) & r2 in ( halfline 0 );

        C = {} by A1, A2, A7, A8, Def4;

        then ( Cl C) = {} by PRE_TOPC: 22;

        hence thesis;

      end;

        suppose r1 in DYADIC & r2 in ( halfline 0 );

        then r2 < 0 & ex s be Nat st r1 in ( dyadic s) by URYSOHN1:def 2, XXREAL_1: 233;

        hence thesis by A4, URYSOHN1: 1;

      end;

        suppose

         A9: r1 in ( right_open_halfline 1) & r2 in ( halfline 0 );

        then 1 < r1 by XXREAL_1: 235;

        hence thesis by A4, A9, XXREAL_1: 233;

      end;

        suppose

         A10: r1 in ( halfline 0 ) & r2 in DYADIC ;

        C = {} by A1, A2, A7, A10, Def4;

        then ( Cl C) = {} by PRE_TOPC: 22;

        hence thesis;

      end;

        suppose

         A11: r1 in DYADIC & r2 in DYADIC ;

        then

        consider n2 be Nat such that

         A12: r2 in ( dyadic n2) by URYSOHN1:def 2;

        consider n1 be Nat such that

         A13: r1 in ( dyadic n1) by A11, URYSOHN1:def 2;

        set n = (n1 + n2);

        

         A14: ( dyadic n1) c= ( dyadic n) by NAT_1: 11, URYSOHN2: 29;

        then

         A15: (( Tempest G) . r1) = ((G . n) . r1) by A1, A2, A11, A13, Def4;

        ( dyadic n2) c= ( dyadic n) by NAT_1: 11, URYSOHN2: 29;

        then

        reconsider r1, r2 as Element of ( dyadic n) by A13, A12, A14;

        reconsider D = (G . n) as Drizzle of A, B, n by A1, Def2;

        ( Cl (D . r1)) c= (D . r2) by A1, A4, Def1;

        hence thesis by A1, A3, A7, A11, A15, Def4;

      end;

        suppose

         A16: r1 in ( right_open_halfline 1) & r2 in DYADIC ;

        then ex s be 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 thesis by A4, A17, XXREAL_0: 2;

      end;

        suppose

         A18: r1 in ( halfline 0 ) & r2 in ( right_open_halfline 1);

        C = {} by A1, A2, A7, A18, Def4;

        then ( Cl C) = {} by PRE_TOPC: 22;

        hence thesis;

      end;

        suppose r1 in DYADIC & r2 in ( right_open_halfline 1);

        then (( Tempest G) . r2) = the carrier of T by A1, A3, Def4;

        hence thesis;

      end;

        suppose r1 in ( right_open_halfline 1) & r2 in ( right_open_halfline 1);

        then (( Tempest G) . r2) = the carrier of T by A1, A3, Def4;

        hence thesis;

      end;

    end;

    definition

      let T be non empty TopSpace, A,B be Subset of T, G be Rain of A, B, p be Point of T;

      :: URYSOHN3:def5

      func Rainbow (p,G) -> Subset of ExtREAL means

      : Def5: for x be set holds x in it iff (x in DYADIC & for s be Real st s = x holds not p in (( Tempest G) . s));

      existence

      proof

        defpred P[ object] means for s be Real st s = $1 holds not p in (( Tempest G) . s);

        consider R be set such that

         A1: for x be object holds x in R iff x in DYADIC & P[x] from XBOOLE_0:sch 1;

        R c= REAL

        proof

          let x be object;

          assume x in R;

          then x in DYADIC by A1;

          hence thesis;

        end;

        then

        reconsider R as Subset of ExtREAL by NUMBERS: 31, XBOOLE_1: 1;

        take R;

        thus thesis by A1;

      end;

      uniqueness

      proof

        let R1,R2 be Subset of ExtREAL such that

         A2: for x be set holds x in R1 iff (x in DYADIC & for s be Real st s = x holds not p in (( Tempest G) . s)) and

         A3: for x be set holds x in R2 iff (x in DYADIC & for s be Real st s = x holds not p in (( Tempest G) . s));

        for x be object holds x in R1 iff x in R2

        proof

          let x be object;

          hereby

            assume x in R1;

            then x in DYADIC & for s be Real st s = x holds not p in (( Tempest G) . s) by A2;

            hence x in R2 by A3;

          end;

          assume x in R2;

          then x in DYADIC & for s be Real st s = x holds not p in (( Tempest G) . s) by A3;

          hence thesis by A2;

        end;

        hence thesis by TARSKI: 2;

      end;

    end

    theorem :: URYSOHN3:13

    

     Th13: for T be non empty TopSpace, A,B be Subset of T, G be Rain of A, B, p be Point of T holds ( Rainbow (p,G)) c= DYADIC by Def5;

    definition

      let T be non empty TopSpace;

      let A,B be Subset of T;

      let R be Rain of A, B;

      :: URYSOHN3:def6

      func Thunder (R) -> Function of T, R^1 means

      : Def6: for p be Point of T holds (( Rainbow (p,R)) = {} implies (it . p) = 0 ) & for S be non empty Subset of ExtREAL st S = ( Rainbow (p,R)) holds (it . p) = ( sup S);

      existence

      proof

        defpred P[ Element of T, set] means ((( Rainbow ($1,R)) = {} implies $2 = 0 ) & (for S be non empty Subset of ExtREAL st S = ( Rainbow ($1,R)) holds $2 = ( sup S)));

        

         A1: for x be Element of T holds ex y be Element of R^1 st P[x, y]

        proof

          let x be Element of T;

          per cases ;

            suppose

             A2: ( Rainbow (x,R)) = {} ;

             0 in REAL by XREAL_0:def 1;

            then

            reconsider y = 0 as Element of R^1 by TOPMETR: 17;

             P[x, y] by A2;

            hence thesis;

          end;

            suppose ( Rainbow (x,R)) <> {} ;

            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 be object such that

             A3: q in S by XBOOLE_0:def 1;

            reconsider q as R_eal by A3;

            

             A4: 0 in REAL by XREAL_0:def 1;

            

             A5: 1 in REAL by XREAL_0:def 1;

            S c= DYADIC by Th13;

            then S c= [. 0. , e1.] by URYSOHN2: 28;

            then

             A6: 0 <= ( inf S) & ( sup S) <= 1 by URYSOHN2: 26;

            ( inf S) <= q & q <= ( sup S) by A3, XXREAL_2: 3, XXREAL_2: 4;

            then ( sup S) in REAL by A6, XXREAL_0: 45, A4, A5;

            then

            reconsider y = ( sup S) as Element of R^1 by TOPMETR: 17;

            take y;

            thus thesis;

          end;

        end;

        ex F be Function of the carrier of T, the carrier of R^1 st for x be Element of T holds P[x, (F . x)] from FUNCT_2:sch 3( A1);

        then

        consider F be Function of T, R^1 such that

         A7: for x be Element of T holds P[x, (F . x)];

        take F;

        thus thesis by A7;

      end;

      uniqueness

      proof

        let G1,G2 be Function of T, R^1 such that

         A8: for p be Point of T holds (( Rainbow (p,R)) = {} implies (G1 . p) = 0 ) & for S be non empty Subset of ExtREAL st S = ( Rainbow (p,R)) holds (G1 . p) = ( sup S) and

         A9: for p be Point of T holds (( Rainbow (p,R)) = {} implies (G2 . p) = 0 ) & for S be non empty Subset of ExtREAL st S = ( Rainbow (p,R)) holds (G2 . p) = ( sup S);

        for x be object st x in the carrier of T holds (G1 . x) = (G2 . x)

        proof

          let x be object;

          assume x in the carrier of T;

          then

          reconsider x as Point of T;

          per cases ;

            suppose

             A10: ( Rainbow (x,R)) = {} ;

            

            then (G1 . x) = 0 by A8

            .= (G2 . x) by A9, A10;

            hence thesis;

          end;

            suppose ( Rainbow (x,R)) <> {} ;

            then

            reconsider S = ( Rainbow (x,R)) as non empty Subset of ExtREAL ;

            (G1 . x) = ( sup S) by A8

            .= (G2 . x) by A9;

            hence thesis;

          end;

        end;

        hence thesis by FUNCT_2: 12;

      end;

    end

    theorem :: URYSOHN3:14

    

     Th14: for T be non empty TopSpace, A,B be Subset of T, G be Rain of A, B, p be Point of T, S be non empty Subset of ExtREAL st S = ( Rainbow (p,G)) holds for e1 be 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, A,B be Subset of T, G be Rain of A, B, p be Point of T, S be non empty Subset of ExtREAL ;

      consider s be object such that

       A1: s in S by XBOOLE_0:def 1;

      reconsider s as R_eal by A1;

      assume S = ( Rainbow (p,G));

      then S c= DYADIC by Th13;

      then

       A2: S c= [.a, b.] by URYSOHN2: 28;

      let e1 be R_eal;

      assume e1 = 1;

      then for x be ExtReal holds x in S implies 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 thesis by A3, A1, XXREAL_2: 4, XXREAL_2:def 3;

    end;

    theorem :: URYSOHN3:15

    

     Th15: for T be non empty normal TopSpace, A,B be closed Subset of T st A <> {} & A misses B holds for G be Rain of A, B, r be Element of DOM , p be Point of T st (( Thunder G) . p) < r holds p in (( Tempest G) . r)

    proof

      let T be non empty normal TopSpace;

      let A,B be closed Subset of T;

      assume

       A1: A <> {} & A misses B;

      let G be Rain of A, B;

      let r be Element of DOM ;

      let p be Point of T;

      assume

       A2: (( Thunder G) . p) < r;

      now

        per cases ;

          suppose

           A3: ( Rainbow (p,G)) = {} ;

          assume

           A4: not 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

            per cases by A6, A5, XXREAL_1: 233;

              suppose

               A7: r in DYADIC ;

              reconsider r1 = r as R_eal by XXREAL_0:def 1;

              

               A8: for s be 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 thesis by A2, A9, XXREAL_2: 4;

            end;

              suppose r in ( right_open_halfline 1);

              then (( Tempest G) . r) = the carrier of T by A1, Def4;

              hence thesis;

            end;

          end;

          hence thesis;

        end;

          suppose ( Rainbow (p,G)) <> {} ;

          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 be object such that

           A10: s in S by XBOOLE_0:def 1;

          reconsider s as R_eal by A10;

          

           A11: s <= ( sup S) by A10, XXREAL_2: 4;

          assume

           A12: not 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 be R_eal st x in S holds 0. <= x & x <= e1

          proof

            let x be R_eal;

            assume x in S;

            then

             A15: x in DYADIC by Def5;

            then

            reconsider x as Real;

            ex n be Nat st x in ( dyadic n) by A15, URYSOHN1:def 2;

            hence thesis by URYSOHN1: 1;

          end;

          then

           A16: 0. <= s by A10;

          now

            per cases by A2, A14, A16, A11, A13, XXREAL_1: 233;

              suppose

               A17: r in DYADIC ;

              reconsider r1 = r as R_eal by XXREAL_0:def 1;

              for s be Real st s = r1 holds not p in (( Tempest G) . s) by A12;

              then r1 in ( Rainbow (p,G)) by A17, Def5;

              hence thesis by A2, A14, XXREAL_2: 4;

            end;

              suppose r in ( right_open_halfline 1);

              then (( Tempest G) . r) = the carrier of T by A1, Def4;

              hence thesis;

            end;

          end;

          hence thesis;

        end;

      end;

      hence thesis;

    end;

    theorem :: URYSOHN3:16

    

     Th16: for T be non empty normal TopSpace, A,B be closed Subset of T st A <> {} & A misses B holds for G be Rain of A, B holds for r be Real st r in ( DYADIC \/ ( right_open_halfline 1)) & 0 < r holds for p be Point of T holds p in (( Tempest G) . r) implies (( Thunder G) . p) <= r

    proof

      let T be non empty normal TopSpace;

      let A,B be closed Subset of T;

      assume

       A1: A <> {} & A misses B;

      let G be Rain of A, B;

      let r be Real;

      assume that

       A2: r in ( DYADIC \/ ( right_open_halfline 1)) and

       A3: 0 < r;

      let p be Point of T;

      assume

       A4: p in (( Tempest G) . r);

      per cases by A2, XBOOLE_0:def 3;

        suppose

         A5: r in DYADIC ;

        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

          per cases ;

            case ( Rainbow (p,G)) = {} ;

            hence thesis by A3, Def6;

          end;

            case ( Rainbow (p,G)) <> {} ;

            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 be ExtReal holds r1 in S implies r1 <= er

            proof

              let r1 be ExtReal;

              assume

               A7: r1 in S;

              assume

               A8: not r1 <= er;

              

               A9: S c= DYADIC by Th13;

              then r1 in DYADIC by A7;

              then

              reconsider p1 = r1 as Real;

              per cases ;

                suppose

                 A10: ( inf_number_dyadic r) <= ( inf_number_dyadic p1);

                set n = ( inf_number_dyadic p1);

                r in ( dyadic n) by A5, A10, Th6;

                then

                 A11: (( Tempest G) . r) = ((G . n) . r) by A1, A5, A6, Def4;

                reconsider D = (G . n) as Drizzle of A, B, n 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 n) by A7, A9, Th5;

                then

                 A13: (( Tempest G) . p1) = ((G . n) . p1) by A1, A7, A9, A12, Def4;

                reconsider r, p1 as Element of ( dyadic n) 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);

                hence thesis by A4, A7, A11, A13, Def5;

              end;

                suppose ( inf_number_dyadic p1) <= ( inf_number_dyadic r);

                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 . n) as Drizzle of A, B, n 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 . n) . p1) by A1, A7, A9, A15, A14, Def4;

                r in ( dyadic n) by A5, Th6;

                then

                 A17: (( Tempest G) . r) = ((G . n) . r) by A1, A5, A6, Def4;

                reconsider p1 as Element of ( dyadic n) by A15, A14;

                reconsider r as Element of ( dyadic n) 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);

                hence thesis by A4, A7, A17, A16, Def5;

              end;

            end;

            then r is UpperBound of S by XXREAL_2:def 1;

            then ( sup S) <= er by XXREAL_2:def 3;

            hence thesis by Def6;

          end;

        end;

        hence thesis;

      end;

        suppose r in ( right_open_halfline 1);

        then

         A18: 1 < r by XXREAL_1: 235;

        now

          per cases ;

            case ( Rainbow (p,G)) = {} ;

            hence thesis by A18, Def6;

          end;

            case

             A19: ( Rainbow (p,G)) <> {} ;

            reconsider e1 = 1 as R_eal by XXREAL_0:def 1;

            consider S be 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 thesis by A18, XXREAL_0: 2;

          end;

        end;

        hence thesis;

      end;

    end;

    theorem :: URYSOHN3:17

    

     Th17: for T be non empty normal TopSpace, A,B be closed Subset of T st A <> {} & A misses B holds for G be Rain of A, B, r1 be Element of DOM st 0 < r1 holds for p be Point of T st r1 < (( Thunder G) . p) holds not p in (( Tempest G) . r1)

    proof

      let T be non empty normal TopSpace;

      let A,B be closed Subset of T;

      assume

       A1: A <> {} & A misses B;

      let G be Rain of A, B;

      let r1 be Element of DOM ;

      assume

       A2: 0 < r1;

      let p be Point of T;

      assume

       A3: r1 < (( Thunder G) . p) & p in (( Tempest G) . r1);

      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 thesis by A1, A2, A3, Th16;

    end;

    theorem :: URYSOHN3:18

    

     Th18: for T be non empty normal TopSpace, A,B be closed Subset of T st A <> {} & A misses B holds for G be Rain of A, B holds ( Thunder G) is continuous & for x be 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;

      let A,B be closed Subset of T;

      assume

       A4: A <> {} & A misses B;

      let G be Rain of A, B;

      

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

        now

          per cases ;

            case

             A9: ( Rainbow (x,G)) = {} ;

            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;

              (( Tempest G) . 1) = ((G . 0 ) . 1) by A4, A1, A2, A3, Def4;

              then for s be Real st s = 1 holds not x in (( Tempest G) . s) by A11, A10, XBOOLE_0:def 5;

              hence thesis by A9, Def5, URYSOHN2: 27;

            end;

            hence thesis by A9, Def6;

          end;

            case

             A12: ( Rainbow (x,G)) <> {} ;

            

             A13: x in A implies (( Thunder G) . x) = 0

            proof

              assume

               A14: x in A;

              

               A15: for s be R_eal st 0. < s holds not s in ( Rainbow (x,G))

              proof

                let s be R_eal;

                assume 0. < s;

                assume

                 A16: s in ( Rainbow (x,G));

                then

                 A17: s in DYADIC by Def5;

                then

                reconsider s as Real;

                consider n be 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;

                per cases by A18, URYSOHN1: 1;

                  suppose

                   A20: s = 0 ;

                  A c= (D . 0 ) by A4, Def1;

                  hence thesis by A14, A16, A19, A20, Def5;

                end;

                  suppose

                   A21: 0 < s;

                  

                   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;

                  A c= (D . 0 ) by A4, Def1;

                  then A c= (D . s) by A23;

                  hence thesis by A14, A16, A19, Def5;

                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 be object such that

               A26: a in ( Rainbow (x,G)) by A12, XBOOLE_0:def 1;

              

               A27: a in DYADIC by A26, Def5;

              then

              reconsider a as Real;

              

               A28: ex n be Nat st a in ( dyadic n) by A27, URYSOHN1:def 2;

              per cases by A28, URYSOHN1: 1;

                suppose a = 0 ;

                hence thesis by A14, A25, A24, A26, Def5;

              end;

                suppose 0 < a;

                hence thesis by A15, A26;

              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;

              (( Tempest G) . 1) = ((G . 0 ) . 1) by A4, A1, A2, A3, Def4;

              then

               A33: for s be 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 thesis by A29, A34, XXREAL_0: 1;

            end;

            e1 = 1 & (( Thunder G) . x) = ( sup S) by Def6;

            hence thesis by A13, A30, Th14;

          end;

        end;

        hence thesis;

      end;

      for p be Point of T holds ( Thunder G) is_continuous_at p

      proof

        let p be Point of T;

        for Q be Subset of R^1 st Q is open & (( Thunder G) . p) in Q holds ex H be Subset of T st H is open & p in H & (( Thunder G) .: H) c= Q

        proof

          let Q be Subset of R^1 ;

          assume that

           A35: Q is open and

           A36: (( Thunder G) . p) in Q;

          reconsider x = (( Thunder G) . p) as Element of RealSpace by A36, TOPMETR: 12, TOPMETR:def 6;

          reconsider 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, TOPMETR: 12, TOPMETR:def 6;

          then

          consider r be Real such that

           A37: r > 0 and

           A38: ( Ball (x,r)) c= Q by A36, PCOMPS_1:def 4;

          ex r0 be Real st r0 < r & 0 < r0 & r0 <= 1

          proof

            per cases ;

              suppose

               A39: r <= 1;

              consider r0 be Real such that

               A40: 0 < r0 & r0 < r by A37, XREAL_1: 5;

              reconsider r0 as Real;

              take r0;

              thus thesis by A39, A40, XXREAL_0: 2;

            end;

              suppose 1 < r;

              hence thesis;

            end;

          end;

          then

          consider r0 be Real such that

           A41: r0 < r and

           A42: 0 < r0 & r0 <= 1;

          consider r1 be 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 be 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 be Point of T holds p in (( Tempest G) . r1) implies (( Thunder G) . p) < r

          proof

            let p be Point of T;

            assume p in (( Tempest G) . r1);

            then (( Thunder G) . p) <= r1 by A4, A44, A46, Th16;

            hence thesis by A50, XXREAL_0: 2;

          end;

          

           A52: the carrier of R^1 = the carrier of RealSpace by TOPMETR: 12, TOPMETR:def 6;

          reconsider 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 be Subset of T st H is open & p in H & (( Thunder G) .: H) c= Q

          proof

            per cases ;

              suppose

               A54: x = 0 ;

              take H;

              (( Thunder G) .: H) c= Q

              proof

                reconsider p = x as Real;

                let y be object;

                assume y in (( Thunder G) .: H);

                then

                consider x1 be object 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 as Point of RealSpace by A52, A55, A56, FUNCT_2: 5;

                reconsider q = y as Real;

                

                 A57: ( - (p - q)) < r by A51, A49, A54, A55, A56;

                reconsider 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: |.(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)) = |.(p - q).| & |.(p - q).| <= r by A54, A56, A58, A59, ABSVALUE: 5, TOPMETR: 11;

                hence thesis by A38, A61, A60, XXREAL_0: 1;

              end;

              hence thesis by A4, A44, A48, A49, A53, A54, Def1, Th15;

            end;

              suppose

               A62: x <> 0 ;

              reconsider x as Real;

               0 <= (( Thunder G) . p) by A8;

              then

              consider r1,r2 be 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 be 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;

              reconsider A = (( Tempest G) . r3) as Subset of T by A69, FUNCT_2: 5;

              take H = (A /\ C);

              

               A73: (( Thunder G) .: H) c= Q

              proof

                reconsider x as Element of RealSpace ;

                let y be object;

                reconsider p = x as Real;

                assume y in (( Thunder G) .: H);

                then

                consider x1 be object 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 as Point of T by A74;

                

                 A76: x1 in (( Tempest G) . r3) by A74, XBOOLE_0:def 4;

                reconsider y as Real by A75;

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

                  hence thesis by A81, A82, XBOOLE_0:def 5;

                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)) = |.(p - q).| & |.(p - q).| <= r by A80, ABSVALUE: 5, TOPMETR: 11;

                

                 A85: |.(p - q).| <> r

                proof

                  assume

                   A86: |.(p - q).| = r;

                  per cases ;

                    suppose 0 <= (p - q);

                    hence thesis by A67, A83, A86, ABSVALUE:def 1;

                  end;

                    suppose (p - q) < 0 ;

                    then |.(p - q).| = ( - (p - q)) by ABSVALUE:def 1;

                    hence thesis by A67, A79, A86;

                  end;

                end;

                ( dist (x,y)) < r implies y in ( Ball (x,r)) by METRIC_1: 11;

                hence thesis by A38, A84, A85, XXREAL_0: 1;

              end;

              (( Thunder G) . p) <= 1 by A8;

              then

              consider r4 be 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 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 thesis by A72, A92, A73, TOPS_1: 11, XBOOLE_0:def 4;

            end;

          end;

          hence thesis;

        end;

        hence thesis by TMAP_1: 43;

      end;

      hence thesis by A8, TMAP_1: 44;

    end;

    theorem :: URYSOHN3:19

    

     Th19: for T be non empty normal TopSpace, A,B be closed Subset of T st A <> {} & A misses B holds ex F be Function of T, R^1 st F is continuous & for x be 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;

      let A,B be closed Subset of T;

      assume

       A1: A <> {} & A misses B;

      set R = the Rain of A, B;

      take ( Thunder R);

      thus thesis by A1, Th18;

    end;

    ::$Notion-Name

    theorem :: URYSOHN3:20

    

     Th20: for T be non empty normal TopSpace, A,B be closed Subset of T st A misses B holds ex F be Function of T, R^1 st F is continuous & for x be 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;

      let A,B be closed Subset of T;

      assume

       A1: A misses B;

      per cases ;

        suppose A <> {} ;

        hence thesis by A1, Th19;

      end;

        suppose

         A2: A = {} ;

        set S = the carrier of T, L = the carrier of R^1 ;

        1 in REAL by XREAL_0:def 1;

        then

        reconsider r = 1 as Element of L by TOPMETR: 17;

        defpred P[ set, set] means $2 = r;

        

         A3: for x be Element of S holds ex y be Element of L st P[x, y];

        ex F be Function of S, L st for x be Element of S holds P[x, (F . x)] from FUNCT_2:sch 3( A3);

        then

        consider F be Function of S, L such that

         A4: for x be Element of S holds (F . x) = r;

        take F;

        

         A5: ( dom F) = the carrier of T by FUNCT_2:def 1;

        thus F is continuous

        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 ;

          assume P is closed;

          

           A6: O2 is closed;

          per cases ;

            suppose 1 in P;

            then for x be object holds x in the carrier of T iff x in ( dom F) & (F . x) in P by A4, FUNCT_2:def 1;

            hence thesis by FUNCT_1:def 7;

          end;

            suppose not 1 in P;

            then for x be object holds x in {} iff x in ( dom F) & (F . x) in P by A4, A5;

            hence thesis by A6, FUNCT_1:def 7;

          end;

        end;

        let x be Point of T;

        thus thesis by A2, A4;

      end;

    end;

    theorem :: URYSOHN3:21

    for T be non empty T_2 compact TopSpace, A,B be closed Subset of T st A misses B holds ex F be Function of T, R^1 st F is continuous & for x be 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;