urysohn1.miz



    begin

    definition

      let n be Nat;

      :: URYSOHN1:def1

      func dyadic (n) -> Subset of REAL means

      : Def1: for x be Real holds x in it iff ex i be Nat st i <= (2 |^ n) & x = (i / (2 |^ n));

      existence

      proof

        defpred P[ set] means ex i be Nat st (i <= (2 |^ n) & $1 = (i / (2 |^ n)));

        consider X be Subset of REAL such that

         A1: for x be Element of REAL holds x in X iff P[x] from SUBSET_1:sch 3;

        take X;

        let x be Real;

        reconsider x as Element of REAL by XREAL_0:def 1;

        x in X iff P[x] by A1;

        hence thesis;

      end;

      uniqueness

      proof

        let A1,A2 be Subset of REAL ;

        assume that

         A2: for x be Real holds x in A1 iff ex i be Nat st i <= (2 |^ n) & x = (i / (2 |^ n)) and

         A3: for x be Real holds x in A2 iff ex i be Nat st i <= (2 |^ n) & x = (i / (2 |^ n));

        for a be object holds a in A1 iff a in A2

        proof

          let a be object;

          thus a in A1 implies a in A2

          proof

            assume

             A4: a in A1;

            then

            reconsider a as Real;

            ex i be Nat st i <= (2 |^ n) & a = (i / (2 |^ n)) by A2, A4;

            hence thesis by A3;

          end;

          assume

           A5: a in A2;

          then

          reconsider a as Real;

          ex i be Nat st i <= (2 |^ n) & a = (i / (2 |^ n)) by A3, A5;

          hence thesis by A2;

        end;

        hence thesis by TARSKI: 2;

      end;

    end

    definition

      :: URYSOHN1:def2

      func DYADIC -> Subset of REAL means

      : Def2: for a be Real holds a in it iff ex n be Nat st a in ( dyadic n);

      existence

      proof

        defpred P[ set] means ex i be Nat st $1 in ( dyadic i);

        consider X be Subset of REAL such that

         A1: for x be Element of REAL holds x in X iff P[x] from SUBSET_1:sch 3;

        take X;

        let a be Real;

        reconsider a as Element of REAL by XREAL_0:def 1;

        a in X iff P[a] by A1;

        hence thesis;

      end;

      uniqueness

      proof

        let A1,A2 be Subset of REAL ;

        assume that

         A2: for x be Real holds x in A1 iff ex n be Nat st x in ( dyadic n) and

         A3: for x be Real holds x in A2 iff ex n be Nat st x in ( dyadic n);

        for a be object holds a in A1 iff a in A2

        proof

          let a be object;

          thus a in A1 implies a in A2

          proof

            assume

             A4: a in A1;

            then

            reconsider a as Real;

            ex n be Nat st a in ( dyadic n) by A2, A4;

            hence thesis by A3;

          end;

          thus a in A2 implies a in A1

          proof

            assume

             A5: a in A2;

            then

            reconsider a as Real;

            ex n be Nat st a in ( dyadic n) by A3, A5;

            hence thesis by A2;

          end;

        end;

        hence thesis by TARSKI: 2;

      end;

    end

    definition

      :: URYSOHN1:def3

      func DOM -> Subset of REAL equals ((( halfline 0 ) \/ DYADIC ) \/ ( right_open_halfline 1));

      coherence ;

    end

    theorem :: URYSOHN1:1

    

     Th1: for n be Nat holds for x be Real st x in ( dyadic n) holds 0 <= x & x <= 1

    proof

      let n be Nat;

      let x be Real;

      assume x in ( dyadic n);

      then

      consider i be Nat such that

       A1: i <= (2 |^ n) and

       A2: x = (i / (2 |^ n)) by Def1;

      ( 0 / (2 |^ n)) <= (i / (2 |^ n)) & (i / (2 |^ n)) <= ((2 |^ n) / (2 |^ n)) by A1, XREAL_1: 72;

      hence thesis by A2, XCMPLX_1: 60;

    end;

    theorem :: URYSOHN1:2

    

     Th2: ( dyadic 0 ) = { 0 , 1}

    proof

      

       A1: (2 |^ 0 ) = 1 by NEWTON: 4;

      

       A2: for x be Real holds x in ( dyadic 0 ) iff ex i be Nat st i <= 1 & x = i

      proof

        let x be Real;

        

         A3: (ex i be Nat st i <= 1 & x = i) implies x in ( dyadic 0 )

        proof

          given i be Nat such that

           A4: i <= 1 and

           A5: x = i;

          x = (i / 1) by A5;

          hence thesis by A1, A4, Def1;

        end;

        x in ( dyadic 0 ) implies ex i be Nat st i <= 1 & x = i

        proof

          assume x in ( dyadic 0 );

          then ex i be Nat st i <= 1 & x = (i / 1) by A1, Def1;

          hence thesis;

        end;

        hence thesis by A3;

      end;

      for x be object holds x in ( dyadic 0 ) iff x in { 0 , 1}

      proof

        let x be object;

        

         A6: x in ( dyadic 0 ) implies x in { 0 , 1}

        proof

          assume

           A7: x in ( dyadic 0 );

          then

          reconsider x as Real;

          consider i be Nat such that

           A8: i <= 1 and

           A9: x = i by A2, A7;

          i <= ( 0 + 1) by A8;

          then x = 0 or x = 1 by A9, NAT_1: 9;

          hence thesis by TARSKI:def 2;

        end;

        x in { 0 , 1} implies x in ( dyadic 0 )

        proof

          assume x in { 0 , 1};

          then x = 0 or x = 1 by TARSKI:def 2;

          hence thesis by A2;

        end;

        hence thesis by A6;

      end;

      hence thesis by TARSKI: 2;

    end;

    theorem :: URYSOHN1:3

    ( dyadic 1) = { 0 , (1 / 2), 1}

    proof

      

       A1: (2 |^ 1) = 2;

      for x be object holds x in ( dyadic 1) iff x in { 0 , (1 / 2), 1}

      proof

        let x be object;

        

         A2: x in { 0 , (1 / 2), 1} implies x in ( dyadic 1)

        proof

          assume

           A3: x in { 0 , (1 / 2), 1};

          per cases by A3, ENUMSET1:def 1;

            suppose x = 0 ;

            then x = ( 0 / 2);

            hence thesis by A1, Def1;

          end;

            suppose x = (1 / 2);

            hence thesis by A1, Def1;

          end;

            suppose

             A4: x = 1;

            then

            reconsider x as Real;

            x = (2 / 2) by A4;

            hence thesis by A1, Def1;

          end;

        end;

        x in ( dyadic 1) implies x in { 0 , (1 / 2), 1}

        proof

          assume

           A5: x in ( dyadic 1);

          then

          reconsider x as Real;

          consider i be Nat such that

           A6: i <= 2 and

           A7: x = (i / 2) by A1, A5, Def1;

          i = 0 or ... or i = 2 by A6;

          hence thesis by A7, ENUMSET1:def 1;

        end;

        hence thesis by A2;

      end;

      hence thesis by TARSKI: 2;

    end;

    registration

      let n be Nat;

      cluster ( dyadic n) -> non empty;

      coherence

      proof

        ex i be Nat st 0 <= i & i <= (2 |^ n) & ( 0 / (2 |^ n)) = (i / (2 |^ n));

        hence thesis by Def1;

      end;

    end

    definition

      let n be Nat;

      :: URYSOHN1:def4

      func dyad (n) -> FinSequence means

      : Def4: ( dom it ) = ( Seg ((2 |^ n) + 1)) & for i be Nat st i in ( dom it ) holds (it . i) = ((i - 1) / (2 |^ n));

      existence

      proof

        deffunc F( Nat) = (($1 - 1) / (2 |^ n));

        consider FS be FinSequence such that

         A1: ( len FS) = ((2 |^ n) + 1) & for i be Nat st i in ( dom FS) holds (FS . i) = F(i) from FINSEQ_1:sch 2;

        take FS;

        thus thesis by A1, FINSEQ_1:def 3;

      end;

      uniqueness

      proof

        let F1,F2 be FinSequence;

        assume that

         A2: ( dom F1) = ( Seg ((2 |^ n) + 1)) and

         A3: for i be Nat st i in ( dom F1) holds (F1 . i) = ((i - 1) / (2 |^ n)) and

         A4: ( dom F2) = ( Seg ((2 |^ n) + 1)) and

         A5: for i be Nat st i in ( dom F2) holds (F2 . i) = ((i - 1) / (2 |^ n));

        consider X be set such that

         A6: X = ( dom F1);

        for k be Nat st k in X holds (F1 . k) = (F2 . k)

        proof

          let k be Nat;

          assume

           A7: k in X;

          

          hence (F1 . k) = ((k - 1) / (2 |^ n)) by A3, A6

          .= (F2 . k) by A2, A4, A5, A6, A7;

        end;

        hence thesis by A2, A4, A6, FINSEQ_1: 13;

      end;

    end

    theorem :: URYSOHN1:4

    for n be Nat holds ( dom ( dyad n)) = ( Seg ((2 |^ n) + 1)) & ( rng ( dyad n)) = ( dyadic n)

    proof

      let n be Nat;

      

       A1: ( dom ( dyad n)) = ( Seg ((2 |^ n) + 1)) by Def4;

      for x be object holds x in ( rng ( dyad n)) iff x in ( dyadic n)

      proof

        let x be object;

        

         A2: x in ( rng ( dyad n)) implies x in ( dyadic n)

        proof

          assume x in ( rng ( dyad n));

          then

          consider y be object such that

           A3: y in ( dom ( dyad n)) and

           A4: x = (( dyad n) . y) by FUNCT_1:def 3;

          

           A5: y in ( Seg ((2 |^ n) + 1)) by A3, Def4;

          reconsider y as Nat by A3;

          

           A6: 1 <= y by A5, FINSEQ_1: 1;

          y <= ((2 |^ n) + 1) by A5, FINSEQ_1: 1;

          then

           A7: (y - 1) <= (((2 |^ n) + 1) - 1) by XREAL_1: 13;

          consider i be Nat such that

           A8: (1 + i) = y by A6, NAT_1: 10;

          i in NAT & x = ((y - 1) / (2 |^ n)) by A3, A4, Def4, ORDINAL1:def 12;

          hence thesis by A7, A8, Def1;

        end;

        x in ( dyadic n) implies x in ( rng ( dyad n))

        proof

          assume

           A9: x in ( dyadic n);

          then

          reconsider x as Real;

          consider i be Nat such that

           A10: i <= (2 |^ n) and

           A11: x = (i / (2 |^ n)) by A9, Def1;

          consider y be Nat such that

           A12: y = (i + 1);

          ( 0 + 1) <= (i + 1) & (i + 1) <= ((2 |^ n) + 1) by A10, XREAL_1: 6;

          then

           A13: y in ( Seg ((2 |^ n) + 1)) by A12, FINSEQ_1: 1;

          then

           A14: y in ( dom ( dyad n)) by Def4;

          x = ((y - 1) / (2 |^ n)) by A11, A12;

          then x = (( dyad n) . y) by A1, A13, Def4;

          hence thesis by A14, FUNCT_1:def 3;

        end;

        hence thesis by A2;

      end;

      hence thesis by Def4, TARSKI: 2;

    end;

    registration

      cluster DYADIC -> non empty;

      coherence

      proof

        ex x be object st x in ( dyadic 0 ) by XBOOLE_0:def 1;

        hence thesis by Def2;

      end;

    end

    registration

      cluster DOM -> non empty;

      coherence ;

    end

    theorem :: URYSOHN1:5

    

     Th5: for n be Nat holds ( dyadic n) c= ( dyadic (n + 1))

    proof

      let n be Nat;

      let x be object;

      assume

       A1: x in ( dyadic n);

      ex i be Nat st i <= (2 |^ (n + 1)) & x = (i / (2 |^ (n + 1)))

      proof

        reconsider x as Real by A1;

        consider i be Nat such that

         A2: i <= (2 |^ n) & x = (i / (2 |^ n)) by A1, Def1;

        take (i * 2);

        (2 |^ (n + 1)) = ((2 |^ n) * 2) by NEWTON: 6;

        hence thesis by A2, XCMPLX_1: 91, XREAL_1: 64;

      end;

      hence thesis by Def1;

    end;

    theorem :: URYSOHN1:6

    

     Th6: for n be Nat holds 0 in ( dyadic n) & 1 in ( dyadic n)

    proof

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

      

       A1: for k be Nat st P[k] holds P[(k + 1)]

      proof

        let k be Nat;

        assume

         A2: 0 in ( dyadic k) & 1 in ( dyadic k);

        ( dyadic k) c= ( dyadic (k + 1)) by Th5;

        hence thesis by A2;

      end;

      

       A3: P[ 0 ] by Th2, TARSKI:def 2;

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

      hence thesis;

    end;

    theorem :: URYSOHN1:7

    

     Th7: for n,i be Nat st 0 < i & i <= (2 |^ n) holds (((i * 2) - 1) / (2 |^ (n + 1))) in (( dyadic (n + 1)) \ ( dyadic n))

    proof

      let n,i be Nat;

      assume that

       A1: 0 < i and

       A2: i <= (2 |^ n);

      ( 0 * 2) < (i * 2) by A1, XREAL_1: 68;

      then

      consider k be Nat such that

       A3: (i * 2) = (k + 1) by NAT_1: 6;

      

       A4: not (((i * 2) - 1) / (2 |^ (n + 1))) in ( dyadic n)

      proof

        assume (((i * 2) - 1) / (2 |^ (n + 1))) in ( dyadic n);

        then

        consider s be Nat such that s <= (2 |^ n) and

         A5: (((i * 2) - 1) / (2 |^ (n + 1))) = (s / (2 |^ n)) by Def1;

        

         A6: (2 |^ n) <> 0 by NEWTON: 83;

        (2 |^ (n + 1)) <> 0 by NEWTON: 83;

        then (((i * 2) - 1) * (2 |^ n)) = (s * (2 |^ (n + 1))) by A5, A6, XCMPLX_1: 95;

        then (((i * 2) - 1) * (2 |^ n)) = (s * ((2 |^ n) * 2)) by NEWTON: 6;

        then (((i * 2) - 1) * (2 |^ n)) = ((s * 2) * (2 |^ n));

        then (((i * 2) - 1) / (2 |^ n)) = ((s * 2) / (2 |^ n)) by A6, XCMPLX_1: 94;

        then ((i * 2) + ( - 1)) = (s * 2) by A6, XCMPLX_1: 53;

        then ((2 * i) + 0 ) = ((2 * s) + 1);

        then 0 = 1 by NAT_1: 18;

        hence thesis;

      end;

      (i * 2) <= ((2 |^ n) * 2) by A2, XREAL_1: 64;

      then (i * 2) <= (2 |^ (n + 1)) by NEWTON: 6;

      then

       A7: k <= (2 |^ (n + 1)) by A3, NAT_1: 13;

      (((i * 2) - 1) / (2 |^ (n + 1))) in ( dyadic (n + 1)) by A3, A7, Def1;

      hence thesis by A4, XBOOLE_0:def 5;

    end;

    theorem :: URYSOHN1:8

    

     Th8: for n,i be Nat st 0 <= i & i < (2 |^ n) holds (((i * 2) + 1) / (2 |^ (n + 1))) in (( dyadic (n + 1)) \ ( dyadic n))

    proof

      let n,i be Nat;

      assume that 0 <= i and

       A1: i < (2 |^ n);

      

       A2: ( 0 + 1) <= (i + 1) by XREAL_1: 6;

      consider s be Nat such that

       A3: s = (i + 1);

      

       A4: ((s * 2) - 1) = ((i * 2) + (1 + 0 )) by A3;

      s <= (2 |^ n) by A1, A3, NAT_1: 13;

      hence thesis by A2, A4, Th7;

    end;

    theorem :: URYSOHN1:9

    

     Th9: for n be Nat holds (1 / (2 |^ (n + 1))) in (( dyadic (n + 1)) \ ( dyadic n))

    proof

      let n be Nat;

      ((2 * 0 ) + 1) = 1 & 0 < (2 |^ n) by NEWTON: 83;

      hence thesis by Th8;

    end;

    definition

      let n be Nat;

      let x be Element of ( dyadic n);

      :: URYSOHN1:def5

      func axis (x) -> Nat means

      : Def5: x = (it / (2 |^ n));

      existence

      proof

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

         A1: x = (i / (2 |^ n)) by Def1;

        take i;

        thus thesis by A1;

      end;

      uniqueness

      proof

        let i1,i2 be Nat;

        assume

         A2: x = (i1 / (2 |^ n)) & x = (i2 / (2 |^ n));

        

         A3: (2 |^ n) <> 0 by NEWTON: 83;

        

        then i1 = ((i1 / (2 |^ n)) * (2 |^ n)) by XCMPLX_1: 87

        .= i2 by A2, A3, XCMPLX_1: 87;

        hence thesis;

      end;

    end

    theorem :: URYSOHN1:10

    

     Th10: for n be Nat holds for x be Element of ( dyadic n) holds x = (( axis x) / (2 |^ n)) & ( axis x) <= (2 |^ n)

    proof

      let n be Nat;

      let x be Element of ( dyadic n);

      ex i be Nat st i <= (2 |^ n) & x = (i / (2 |^ n)) by Def1;

      hence thesis by Def5;

    end;

    theorem :: URYSOHN1:11

    for n be Nat holds for x be Element of ( dyadic n) holds ((( axis x) - 1) / (2 |^ n)) < x & x < ((( axis x) + 1) / (2 |^ n))

    proof

      let n be Nat;

      let x be Element of ( dyadic n);

      

       A1: ( 0 + ( axis x)) < (1 + ( axis x)) & 0 < (2 |^ n) by NEWTON: 83, XREAL_1: 8;

      x = (( axis x) / (2 |^ n)) & (( - 1) + ( axis x)) < ( 0 + ( axis x)) by Def5, XREAL_1: 8;

      hence thesis by A1, XREAL_1: 74;

    end;

    theorem :: URYSOHN1:12

    

     Th12: for n be Nat holds for x be Element of ( dyadic n) holds ((( axis x) - 1) / (2 |^ n)) < ((( axis x) + 1) / (2 |^ n))

    proof

      let n be Nat;

      let x be Element of ( dyadic n);

      (( - 1) + ( axis x)) < (1 + ( axis x)) & 0 < (2 |^ n) by NEWTON: 83, XREAL_1: 8;

      hence thesis by XREAL_1: 74;

    end;

    theorem :: URYSOHN1:13

    

     Th13: for n be Nat holds for x be Element of ( dyadic (n + 1)) holds ( not x in ( dyadic n) implies ((( axis x) - 1) / (2 |^ (n + 1))) in ( dyadic n) & ((( axis x) + 1) / (2 |^ (n + 1))) in ( dyadic n))

    proof

      let n be Nat;

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

      assume

       A1: not x in ( dyadic n);

      thus ((( axis x) - 1) / (2 |^ (n + 1))) in ( dyadic n)

      proof

        consider a be Real such that

         A2: a = ((( axis x) - 1) / (2 |^ (n + 1)));

        ex i be Nat st i <= (2 |^ n) & a = (i / (2 |^ n))

        proof

          consider s be Nat such that

           A3: s <= (2 |^ (n + 1)) and

           A4: x = (s / (2 |^ (n + 1))) by Def1;

          consider k be Element of NAT such that

           A5: s = (2 * k) or s = ((2 * k) + 1) by SCHEME1: 1;

          now

            per cases by A5;

              case

               A6: s = (k * 2);

              then x = ((k * 2) / ((2 |^ n) * 2)) by A4, NEWTON: 6;

              then

               A7: x = (k / (2 |^ n)) by XCMPLX_1: 91;

              (k * 2) <= ((2 |^ n) * 2) by A3, A6, NEWTON: 6;

              then k <= (((2 |^ n) * 2) / 2) by XREAL_1: 77;

              hence thesis by A1, A7, Def1;

            end;

              case

               A8: s = ((k * 2) + 1);

              

               A9: ((2 |^ (n + 1)) - 1) <= (2 |^ (n + 1)) by XREAL_1: 44;

              (k * 2) <= ((2 |^ (n + 1)) - 1) by A3, A8, XREAL_1: 19;

              then (k * 2) <= (2 |^ (n + 1)) by A9, XXREAL_0: 2;

              then (k * 2) <= ((2 |^ n) * 2) by NEWTON: 6;

              then

               A10: k <= (((2 |^ n) * 2) / 2) by XREAL_1: 77;

              take k;

              a = ((((k * 2) + 1) - 1) / (2 |^ (n + 1))) by A2, A4, A8, Def5

              .= ((k * 2) / ((2 |^ n) * 2)) by NEWTON: 6

              .= ((k / (2 |^ n)) * (2 / 2)) by XCMPLX_1: 76

              .= (k / (2 |^ n));

              hence thesis by A10;

            end;

          end;

          hence thesis;

        end;

        hence thesis by A2, Def1;

      end;

      thus ((( axis x) + 1) / (2 |^ (n + 1))) in ( dyadic n)

      proof

        set a = ((( axis x) + 1) / (2 |^ (n + 1)));

        ex i be Nat st i <= (2 |^ n) & a = (i / (2 |^ n))

        proof

          consider s be Nat such that

           A11: s <= (2 |^ (n + 1)) and

           A12: x = (s / (2 |^ (n + 1))) by Def1;

          consider k be Element of NAT such that

           A13: s = (2 * k) or s = ((2 * k) + 1) by SCHEME1: 1;

          now

            per cases by A13;

              case

               A14: s = (k * 2);

              then x = ((k * 2) / ((2 |^ n) * 2)) by A12, NEWTON: 6;

              then

               A15: x = (k / (2 |^ n)) by XCMPLX_1: 91;

              (k * 2) <= ((2 |^ n) * 2) by A11, A14, NEWTON: 6;

              then k <= (((2 |^ n) * 2) / 2) by XREAL_1: 77;

              hence thesis by A1, A15, Def1;

            end;

              case

               A16: s = ((k * 2) + 1);

              consider l be Nat such that

               A17: l = (k + 1);

              s <> (2 |^ (n + 1))

              proof

                

                 A18: (2 |^ (n + 1)) <> 0 by NEWTON: 83;

                assume s = (2 |^ (n + 1));

                then x = 1 by A12, A18, XCMPLX_1: 60;

                hence thesis by A1, Th6;

              end;

              then ((((k * 2) + 1) + 1) + ( - 1)) < (2 |^ (n + 1)) by A11, A16, XXREAL_0: 1;

              then (l * 2) <= (2 |^ (n + 1)) by A17, NAT_1: 13;

              then (l * 2) <= ((2 |^ n) * 2) by NEWTON: 6;

              then

               A19: l <= (((2 |^ n) * 2) / 2) by XREAL_1: 77;

              take l;

              a = ((((k * 2) + 1) + 1) / (2 |^ (n + 1))) by A12, A16, Def5

              .= (((k + 1) * 2) / ((2 |^ n) * 2)) by NEWTON: 6

              .= (((k + 1) / (2 |^ n)) * (2 / 2)) by XCMPLX_1: 76

              .= (l / (2 |^ n)) by A17;

              hence thesis by A19;

            end;

          end;

          hence thesis;

        end;

        hence thesis by Def1;

      end;

    end;

    theorem :: URYSOHN1:14

    

     Th14: for n be Nat holds for x1,x2 be Element of ( dyadic n) st x1 < x2 holds ( axis x1) < ( axis x2)

    proof

      let n be Nat;

      let x1,x2 be Element of ( dyadic n);

      x1 = (( axis x1) / (2 |^ n)) & x2 = (( axis x2) / (2 |^ n)) by Th10;

      hence thesis by XREAL_1: 72;

    end;

    theorem :: URYSOHN1:15

    

     Th15: for n be Nat holds for x1,x2 be Element of ( dyadic n) st x1 < x2 holds x1 <= ((( axis x2) - 1) / (2 |^ n)) & ((( axis x1) + 1) / (2 |^ n)) <= x2

    proof

      let n be Nat;

      let x1,x2 be Element of ( dyadic n);

      assume

       A1: x1 < x2;

      then ( axis x1) < ( axis x2) by Th14;

      then

       A2: (( axis x1) + 1) <= ( axis x2) by NAT_1: 13;

      ( axis x1) < ( axis x2) by A1, Th14;

      then (( axis x1) + 1) <= ( axis x2) by NAT_1: 13;

      then

       A3: ( axis x1) <= (( axis x2) - 1) by XREAL_1: 19;

      

       A4: ((( axis x1) + 1) / (2 |^ n)) <= (( axis x2) / (2 |^ n)) by A2, XREAL_1: 72;

      (( axis x1) / (2 |^ n)) <= ((( axis x2) - 1) / (2 |^ n)) by A3, XREAL_1: 72;

      hence thesis by A4, Th10;

    end;

    theorem :: URYSOHN1:16

    

     Th16: for n be Nat holds for x1,x2 be Element of ( dyadic (n + 1)) st x1 < x2 & not x1 in ( dyadic n) & not x2 in ( dyadic n) holds ((( axis x1) + 1) / (2 |^ (n + 1))) <= ((( axis x2) - 1) / (2 |^ (n + 1)))

    proof

      let n be Nat;

      let x1,x2 be Element of ( dyadic (n + 1));

      assume that

       A1: x1 < x2 and

       A2: not x1 in ( dyadic n) and

       A3: not x2 in ( dyadic n);

      consider k2 be Element of NAT such that

       A4: ( axis x2) = (2 * k2) or ( axis x2) = ((2 * k2) + 1) by SCHEME1: 1;

      

       A5: ( axis x2) <> (k2 * 2)

      proof

        assume

         A6: ( axis x2) = (k2 * 2);

        then x2 = ((k2 * 2) / (2 |^ (n + 1))) by Th10;

        

        then

         A7: x2 = ((k2 * 2) / ((2 |^ n) * 2)) by NEWTON: 6

        .= ((k2 / (2 |^ n)) * (2 / 2)) by XCMPLX_1: 76

        .= (k2 / (2 |^ n));

        (k2 * 2) <= (2 |^ (n + 1)) by A6, Th10;

        then (k2 * 2) <= ((2 |^ n) * 2) by NEWTON: 6;

        then k2 <= (((2 |^ n) * 2) / 2) by XREAL_1: 77;

        hence thesis by A3, A7, Def1;

      end;

      consider k1 be Element of NAT such that

       A8: ( axis x1) = (2 * k1) or ( axis x1) = ((2 * k1) + 1) by SCHEME1: 1;

      

       A9: not ( axis x1) = (k1 * 2)

      proof

        assume

         A10: ( axis x1) = (k1 * 2);

        then x1 = ((k1 * 2) / (2 |^ (n + 1))) by Th10;

        

        then

         A11: x1 = ((k1 * 2) / ((2 |^ n) * 2)) by NEWTON: 6

        .= ((k1 / (2 |^ n)) * (2 / 2)) by XCMPLX_1: 76

        .= (k1 / (2 |^ n));

        (k1 * 2) <= (2 |^ (n + 1)) by A10, Th10;

        then (k1 * 2) <= ((2 |^ n) * 2) by NEWTON: 6;

        then k1 <= (((2 |^ n) * 2) / 2) by XREAL_1: 77;

        hence thesis by A2, A11, Def1;

      end;

      then ((k1 * 2) + 1) < ((k2 * 2) + 1) by A1, A8, A4, A5, Th14;

      then (((k1 * 2) + 1) + ( - 1)) < (((k2 * 2) + 1) + ( - 1)) by XREAL_1: 6;

      then ((k1 * 2) / 2) < ((k2 * 2) / 2) by XREAL_1: 74;

      then (k1 + 1) <= k2 by NAT_1: 13;

      then 0 < (2 |^ (n + 1)) & ((k1 + 1) * 2) <= (k2 * 2) by NEWTON: 83, XREAL_1: 64;

      hence thesis by A8, A4, A9, A5, XREAL_1: 72;

    end;

    begin

    notation

      let T be non empty TopSpace;

      let x be Point of T;

      synonym Nbhd of x,T for a_neighborhood of x;

    end

    definition

      let T be non empty TopSpace;

      let x be Point of T;

      :: original: Nbhd

      redefine

      :: URYSOHN1:def6

      mode Nbhd of x,T means ex A be Subset of T st A is open & x in A & A c= it ;

      compatibility

      proof

        let S be Subset of T;

        hereby

          assume

           A1: S is a_neighborhood of x;

          take N = ( Int S);

          thus N is open;

          thus x in N by A1, CONNSP_2:def 1;

          thus N c= S by TOPS_1: 16;

        end;

        assume ex A be Subset of T st A is open & x in A & A c= S;

        hence x in ( Int S) by TOPS_1: 22;

      end;

    end

    theorem :: URYSOHN1:17

    

     Th17: for T be non empty TopSpace holds for A be Subset of T holds A is open iff for x be Point of T holds x in A implies ex B be Nbhd of x, T st B c= A

    proof

      let T be non empty TopSpace;

      let A be Subset of T;

      thus A is open implies for x be Point of T st x in A holds ex B be Nbhd of x, T st B c= A

      proof

        assume

         A1: A is open;

        let x be Point of T;

        assume x in A;

        then ex B be Subset of T st B is a_neighborhood of x & B c= A by A1, CONNSP_2: 7;

        hence thesis;

      end;

      assume

       A2: for x be Point of T holds x in A implies ex B be Nbhd of x, T st B c= A;

      for x be Point of T st x in A holds ex B be Subset of T st B is a_neighborhood of x & B c= A

      proof

        let x be Point of T;

        assume x in A;

        then ex B be Nbhd of x, T st B c= A by A2;

        hence thesis;

      end;

      hence thesis by CONNSP_2: 7;

    end;

    theorem :: URYSOHN1:18

    for T be non empty TopSpace holds for A be Subset of T holds (for x be Point of T st x in A holds A is Nbhd of x, T) implies A is open

    proof

      let T be non empty TopSpace;

      let A be Subset of T;

      assume

       A1: for x be Point of T st x in A holds A is Nbhd of x, T;

      for x be Point of T holds x in A implies ex B be Nbhd of x, T st B c= A

      proof

        let x be Point of T;

        assume

         A2: x in A;

        ex B be Nbhd of x, T st B c= A

        proof

          A is Nbhd of x, T by A1, A2;

          then

          consider B be Nbhd of x, T such that

           A3: B = A;

          take B;

          thus thesis by A3;

        end;

        hence thesis;

      end;

      hence thesis by Th17;

    end;

    definition

      let T be TopSpace;

      :: original: T_1

      redefine

      :: URYSOHN1:def7

      attr T is T_1 means for p,q be Point of T st not p = q holds ex W,V be Subset of T st W is open & V is open & p in W & not q in W & q in V & not p in V;

      compatibility

      proof

        thus T is T_1 implies for p,q be Point of T st not p = q holds ex W,V be Subset of T st W is open & V is open & p in W & not q in W & q in V & not p in V

        proof

          assume

           A1: T is T_1;

          let p,q be Point of T such that

           A2: not p = q;

          consider G1 be Subset of T such that

           A3: G1 is open & p in G1 & q in (G1 ` ) by A1, A2;

          consider G2 be Subset of T such that

           A4: G2 is open & q in G2 & p in (G2 ` ) by A1, A2;

          take G1, G2;

          thus thesis by A3, A4, XBOOLE_0:def 5;

        end;

        assume

         A5: for p,q be Point of T st not p = q holds ex W,V be Subset of T st W is open & V is open & p in W & not q in W & q in V & not p in V;

        let p,q be Point of T;

        assume p <> q;

        then

        consider W,V be Subset of T such that

         A6: W is open and V is open and

         A7: p in W & not q in W and q in V and not p in V by A5;

        take W;

        thus thesis by A6, A7, XBOOLE_0:def 5;

      end;

    end

    theorem :: URYSOHN1:19

    

     Th19: for T be non empty TopSpace holds T is T_1 iff for p be Point of T holds {p} is closed

    proof

      let T be non empty TopSpace;

      thus T is T_1 implies for p be Point of T holds {p} is closed

      proof

        assume

         A1: T is T_1;

        for p be Point of T holds {p} is closed

        proof

          let p be Point of T;

          consider B be Subset of T such that

           A2: B = ( {p} ` );

          defpred Q[ Subset of T] means ex q be Point of T st (q in B & for V be Subset of T st $1 = V holds (V is open & q in V & not p in V));

          consider F be Subset-Family of T such that

           A3: for C be Subset of T holds C in F iff Q[C] from SUBSET_1:sch 3;

          

           A4: for C be Subset of T holds (C in F iff ex q be Point of T st q in B & C is open & q in C & not p in C)

          proof

            let C be Subset of T;

            

             A5: (ex q be Point of T st (q in B & C is open & q in C & not p in C)) implies C in F

            proof

              assume

               A6: ex q be Point of T st q in B & C is open & q in C & not p in C;

              ex q be Point of T st (q in B & for V be Subset of T st C = V holds V is open & q in V & not p in V)

              proof

                consider q be Point of T such that

                 A7: q in B & C is open & q in C & not p in C by A6;

                take q;

                thus thesis by A7;

              end;

              hence thesis by A3;

            end;

            C in F implies ex q be Point of T st q in B & C is open & q in C & not p in C

            proof

              assume C in F;

              then

              consider q be Point of T such that

               A8: q in B & for V be Subset of T st C = V holds V is open & q in V & not p in V by A3;

              take q;

              thus thesis by A8;

            end;

            hence thesis by A5;

          end;

          for x be object holds x in F implies x in the topology of T

          proof

            let x be object;

            assume

             A9: x in F;

            then

            reconsider x as Subset of T;

            ex q be Point of T st q in B & x is open & q in x & not p in x by A4, A9;

            hence thesis;

          end;

          then

           A10: F c= the topology of T;

          

           A11: for q be Point of T st q in B holds ex V be Subset of T st V is open & q in V & not p in V

          proof

            let q be Point of T;

            assume q in B;

            then not q in {p} by A2, XBOOLE_0:def 5;

            then not q = p by TARSKI:def 1;

            then ex V,W be Subset of T st V is open & W is open & q in V & not p in V & p in W & not q in W by A1;

            then

            consider V be Subset of T such that

             A12: V is open & q in V & not p in V;

            take V;

            thus thesis by A12;

          end;

          for x be object holds x in B implies x in ( union F)

          proof

            let x be object;

            assume

             A13: x in B;

            then

            reconsider x as Point of T;

            consider C be Subset of T such that

             A14: C is open & x in C & not p in C by A11, A13;

            ex C be set st x in C & C in F by A4, A13, A14;

            hence thesis by TARSKI:def 4;

          end;

          then

           A15: B c= ( union F);

          for x be object holds x in ( union F) implies x in B

          proof

            let x be object;

            assume x in ( union F);

            then

            consider C be set such that

             A16: x in C and

             A17: C in F by TARSKI:def 4;

            reconsider C as Subset of T by A17;

            ex q be Point of T st q in B & C is open & q in C & not p in C by A4, A17;

            then C c= (( [#] T) \ {p}) by ZFMISC_1: 34;

            hence thesis by A2, A16;

          end;

          then ( union F) c= B;

          then B = ( union F) by A15;

          then B in the topology of T by A10, PRE_TOPC:def 1;

          then ( {p} ` ) = (( [#] T) \ {p}) & B is open;

          hence thesis by A2;

        end;

        hence thesis;

      end;

      assume

       A18: for p be Point of T holds {p} is closed;

      for p,q be Point of T st not p = q holds ex W,V be Subset of T st W is open & V is open & p in W & not q in W & q in V & not p in V

      proof

        let p,q be Point of T;

        consider V,W be Subset of T such that

         A19: V = ( {p} ` ) and

         A20: W = ( {q} ` );

        p in {p} by TARSKI:def 1;

        then

         A21: not p in V by A19, XBOOLE_0:def 5;

        assume

         A22: not p = q;

        then not p in {q} by TARSKI:def 1;

        then

         A23: p in W by A20, XBOOLE_0:def 5;

        q in {q} by TARSKI:def 1;

        then

         A24: not q in W by A20, XBOOLE_0:def 5;

         not q in {p} by A22, TARSKI:def 1;

        then

         A25: q in V by A19, XBOOLE_0:def 5;

         {p} is closed & {q} is closed by A18;

        hence thesis by A19, A20, A23, A24, A25, A21;

      end;

      hence thesis;

    end;

    theorem :: URYSOHN1:20

    

     Th20: for T be non empty TopSpace st T is normal holds for A,B be open Subset of T st A <> {} & ( Cl A) c= B holds ex C be Subset of T st C <> {} & C is open & ( Cl A) c= C & ( Cl C) c= B

    proof

      let T be non empty TopSpace;

      assume

       A1: T is normal;

      let A,B be open Subset of T;

      assume that

       A2: A <> {} and

       A3: ( Cl A) c= B;

      now

        per cases ;

          case

           A4: B <> ( [#] T);

          reconsider W = ( Cl A), V = (( [#] T) \ B) as Subset of T;

          

           A5: W <> {} & V <> {}

          proof

            

             A6: (( [#] T) \ B) <> {}

            proof

              assume (( [#] T) \ B) = {} ;

              then B = (( [#] T) \ {} ) by PRE_TOPC: 3;

              hence thesis by A4;

            end;

            A c= ( Cl A) by PRE_TOPC: 18;

            hence thesis by A2, A6;

          end;

          

           A7: W misses V

          proof

            assume W meets V;

            then

            consider x be object such that

             A8: x in (W /\ V) by XBOOLE_0: 4;

            x in ( Cl A) & x in (( [#] T) \ B) by A8, XBOOLE_0:def 4;

            hence thesis by A3, XBOOLE_0:def 5;

          end;

          B = (( [#] T) \ V) by PRE_TOPC: 3;

          then V is closed;

          then

          consider C,Q be Subset of T such that

           A9: C is open and

           A10: Q is open and

           A11: W c= C and

           A12: V c= Q and

           A13: C misses Q by A1, A7;

          take C;

          C <> {} & ( Cl A) c= C & ( Cl C) c= B

          proof

            consider Q0,C0 be Subset of ( [#] T) such that

             A14: Q0 = Q & C0 = C;

            C0 c= (Q0 ` ) by A13, A14, SUBSET_1: 23;

            then ( Cl C) c= (Q ` ) by A10, A14, TOPS_1: 5;

            then ( Cl C) misses Q by SUBSET_1: 23;

            then

             A15: V misses ( Cl C) by A12, XBOOLE_1: 63;

            ((B ` ) ` ) = B;

            hence thesis by A5, A11, A15, SUBSET_1: 23;

          end;

          hence thesis by A9;

        end;

          case

           A16: B = ( [#] T);

          consider C be Subset of T such that

           A17: C = ( [#] T);

          take C;

          ( Cl C) c= B by A16;

          hence thesis by A17;

        end;

      end;

      hence thesis;

    end;

    theorem :: URYSOHN1:21

    for T be non empty TopSpace holds T is regular iff for A be open Subset of T holds for p be Point of T st p in A holds ex B be open Subset of T st p in B & ( Cl B) c= A

    proof

      let T be non empty TopSpace;

      thus T is regular implies for A be open Subset of T holds for p be Point of T st p in A holds ex B be open Subset of T st p in B & ( Cl B) c= A

      proof

        assume

         A1: T is regular;

        thus for A be open Subset of T holds for p be Point of T st p in A holds ex B be open Subset of T st p in B & ( Cl B) c= A

        proof

          let A be open Subset of T;

          let p be Point of T;

          assume

           A2: p in A;

          then

           A3: p in ((A ` ) ` );

          thus ex B be open Subset of T st p in B & ( Cl B) c= A

          proof

            reconsider P = (A ` ) as Subset of T;

            now

              per cases ;

                case P <> {} ;

                consider W,V be Subset of T such that

                 A4: W is open and

                 A5: V is open and

                 A6: p in W and

                 A7: P c= V and

                 A8: W misses V by A1, A3;

                (W /\ V) = {} by A8;

                then (V /\ ( Cl W)) c= ( Cl ( {} T)) by A5, TOPS_1: 13;

                then (V /\ ( Cl W)) c= {} by PRE_TOPC: 22;

                then (V /\ ( Cl W)) = {} ;

                then V misses ( Cl W);

                then

                 A9: P misses ( Cl W) by A7, XBOOLE_1: 63;

                take W;

                ((A ` ) ` ) = A;

                then ( Cl W) c= A by A9, SUBSET_1: 23;

                hence thesis by A4, A6;

              end;

                case

                 A10: P = {} ;

                take A;

                A = ( [#] T) by A10, PRE_TOPC: 4;

                then ( Cl A) c= A;

                hence thesis by A2;

              end;

            end;

            hence thesis;

          end;

        end;

      end;

      assume

       A11: for A be open Subset of T holds for p be Point of T st p in A holds ex B be open Subset of T st p in B & ( Cl B) c= A;

      for p be Point of T holds for P be Subset of T st P <> {} & P is closed & p in (P ` ) holds ex W,V be Subset of T st W is open & V is open & p in W & P c= V & W misses V

      proof

        let p be Point of T;

        let P be Subset of T;

        assume that P <> {} and

         A12: P is closed & p in (P ` );

        thus ex W,V be Subset of T st W is open & V is open & p in W & P c= V & W misses V

        proof

          consider A be Subset of T such that

           A13: A = (P ` );

          consider B be open Subset of T such that

           A14: p in B & ( Cl B) c= A by A11, A12, A13;

          consider C be Subset of T such that

           A15: C = (( [#] T) \ ( Cl B));

          reconsider B, C as Subset of T;

          ( Cl B) misses C by A15, XBOOLE_1: 79;

          then

           A16: B misses C by PRE_TOPC: 18, XBOOLE_1: 63;

          take B;

          take C;

          (( Cl B) ` ) is open & ((P ` ) ` ) = P;

          hence thesis by A13, A14, A15, A16, XBOOLE_1: 34;

        end;

      end;

      hence T is regular by COMPTS_1:def 2;

    end;

    theorem :: URYSOHN1:22

    for T be non empty TopSpace st T is normal & T is T_1 holds for A be open Subset of T st A <> {} holds ex B be Subset of T st B <> {} & ( Cl B) c= A

    proof

      let T be non empty TopSpace;

      assume that

       A1: T is normal and

       A2: T is T_1;

      let A be open Subset of T;

      assume

       A3: A <> {} ;

      now

        per cases ;

          case A <> ( [#] T);

          reconsider V = (( [#] T) \ A) as Subset of T;

          consider x be object such that

           A4: x in A by A3, XBOOLE_0:def 1;

          A = (( [#] T) \ V) by PRE_TOPC: 3;

          then

           A5: V is closed;

          reconsider x as Point of T by A4;

          consider W be set such that

           A6: W = {x};

          reconsider W as Subset of T by A6;

          

           A7: W misses V

          proof

            assume W meets V;

            then

            consider z be object such that

             A8: z in (W /\ V) by XBOOLE_0: 4;

            z in W by A8, XBOOLE_0:def 4;

            then

             A9: z in A by A4, A6, TARSKI:def 1;

            z in V by A8, XBOOLE_0:def 4;

            hence thesis by A9, XBOOLE_0:def 5;

          end;

          W is closed by A2, A6, Th19;

          then

          consider B,Q be Subset of T such that B is open and

           A10: Q is open and

           A11: W c= B and

           A12: V c= Q and

           A13: B misses Q by A1, A5, A7;

          take B;

          B <> {} & ( Cl B) c= A

          proof

            B c= (Q ` ) by A13, SUBSET_1: 23;

            then ( Cl B) c= (Q ` ) by A10, TOPS_1: 5;

            then ( Cl B) misses Q by SUBSET_1: 23;

            then

             A14: V misses ( Cl B) by A12, XBOOLE_1: 63;

            ((A ` ) ` ) = A;

            hence thesis by A6, A11, A14, SUBSET_1: 23;

          end;

          hence thesis;

        end;

          case

           A15: A = ( [#] T);

          consider B be Subset of T such that

           A16: B = ( [#] T);

          take B;

          ( Cl B) c= A by A15;

          hence thesis by A16;

        end;

      end;

      hence thesis;

    end;

    theorem :: URYSOHN1:23

    for T be non empty TopSpace st T is normal holds for A,B be Subset of T st A is open & B is closed & B <> {} & B c= A holds ex C be Subset of T st C is open & B c= C & ( Cl C) c= A

    proof

      let T be non empty TopSpace;

      assume

       A1: T is normal;

      let A,B be Subset of T such that

       A2: A is open and

       A3: B is closed & B <> {} and

       A4: B c= A;

      per cases ;

        suppose A <> ( [#] T);

        reconsider V = (( [#] T) \ A) as Subset of T;

        

         A5: A = (( [#] T) \ V) by PRE_TOPC: 3;

        

         A6: B misses V

        proof

          assume (B /\ V) <> {} ;

          then

          consider z be object such that

           A7: z in (B /\ V) by XBOOLE_0:def 1;

          z in B & z in V by A7, XBOOLE_0:def 4;

          hence thesis by A4, XBOOLE_0:def 5;

        end;

        V is closed by A2, A5;

        then

        consider C,Q be Subset of T such that

         A8: C is open and

         A9: Q is open and

         A10: B c= C and

         A11: V c= Q and

         A12: C misses Q by A1, A3, A6;

        C c= (Q ` ) by A12, SUBSET_1: 23;

        then ( Cl C) c= (Q ` ) by A9, TOPS_1: 5;

        then Q misses ( Cl C) by SUBSET_1: 23;

        then

         A13: V misses ( Cl C) by A11, XBOOLE_1: 63;

        take C;

        thus C is open & B c= C by A8, A10;

        ((A ` ) ` ) = A;

        hence thesis by A13, SUBSET_1: 23;

      end;

        suppose

         A14: A = ( [#] T);

        take ( [#] T);

        thus thesis by A14;

      end;

    end;

    begin

    definition

      let T be non empty TopSpace;

      let A,B be Subset of T;

      assume

       A1: T is normal & A <> {} & A is open & B is open & ( Cl A) c= B;

      :: URYSOHN1:def8

      mode Between of A,B -> Subset of T means

      : Def8: it <> {} & it is open & ( Cl A) c= it & ( Cl it ) c= B;

      existence by A1, Th20;

    end

    theorem :: URYSOHN1:24

    for T be non empty TopSpace st T is normal holds for A,B be closed Subset of T st A <> {} holds for n be Nat holds for 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) holds ex F be Function of ( dyadic (n + 1)), ( bool the carrier of T) st 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))

    proof

      let T be non empty TopSpace such that

       A1: T is normal;

      let A,B be closed Subset of T such that

       A2: A <> {} ;

      let n be Nat;

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

       A3: A c= (G . 0 ) and

       A4: B = (( [#] T) \ (G . 1)) and

       A5: 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);

      

       A6: for r be Element of ( dyadic n) holds (G . r) <> {}

      proof

        let r be Element of ( dyadic n);

        per cases by Th1;

          suppose 0 = r;

          hence thesis by A2, A3;

        end;

          suppose

           A7: 0 < r;

          reconsider q1 = 0 as Element of ( dyadic n) by Th6;

          (G . q1) c= ( Cl (G . q1)) & ( Cl (G . q1)) c= (G . r) by A5, A7, PRE_TOPC: 18;

          hence thesis by A2, A3;

        end;

      end;

      reconsider S = (( dyadic (n + 1)) \ ( dyadic n)) as non empty set by Th9;

      

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

      defpred P[ Element of S, Subset of T] means for r be Element of ( dyadic (n + 1)) st r in S & $1 = r holds for r1,r2 be Element of ( dyadic n) st r1 = ((( axis r) - 1) / (2 |^ (n + 1))) & r2 = ((( axis r) + 1) / (2 |^ (n + 1))) holds $2 is Between of (G . r1), (G . r2);

      

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

      proof

        let x be Element of S;

        

         A10: not x in ( dyadic n) by XBOOLE_0:def 5;

        reconsider x as Element of ( dyadic (n + 1)) by XBOOLE_0:def 5;

        ((( axis x) - 1) / (2 |^ (n + 1))) in ( dyadic n) & ((( axis x) + 1) / (2 |^ (n + 1))) in ( dyadic n) by A10, Th13;

        then

        consider q1,q2 be Element of ( dyadic n) such that

         A11: q1 = ((( axis x) - 1) / (2 |^ (n + 1))) & q2 = ((( axis x) + 1) / (2 |^ (n + 1)));

        take the Between of (G . q1), (G . q2);

        thus thesis by A11;

      end;

      consider D be Function of S, ( bool the carrier of T) such that

       A12: for x be Element of S holds P[x, (D . x)] from FUNCT_2:sch 3( A9);

      defpred W[ Element of ( dyadic (n + 1)), Subset of T] means for r be Element of ( dyadic (n + 1)) st $1 = r holds ((r in ( dyadic n) implies $2 = (G . r)) & ( not r in ( dyadic n) implies $2 = (D . r)));

      

       A13: for x be Element of ( dyadic (n + 1)) holds ex y be Subset of T st W[x, y]

      proof

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

        per cases ;

          suppose x in ( dyadic n);

          then

          reconsider x as Element of ( dyadic n);

          consider y be Subset of T such that

           A14: y = (G . x);

          take y;

          thus thesis by A14;

        end;

          suppose

           A15: not x in ( dyadic n);

          then

          reconsider x as Element of S by XBOOLE_0:def 5;

          consider y be Subset of T such that

           A16: y = (D . x);

          take y;

          thus thesis by A15, A16;

        end;

      end;

      consider F be Function of ( dyadic (n + 1)), ( bool the carrier of T) such that

       A17: for x be Element of ( dyadic (n + 1)) holds W[x, (F . x)] from FUNCT_2:sch 3( A13);

      take F;

       0 in ( dyadic n) & 1 in ( dyadic n) by Th6;

      hence A c= (F . 0 ) & B = (( [#] T) \ (F . 1)) by A3, A4, A17, A8;

      let r1,r2,r be Element of ( dyadic (n + 1)) such that

       A18: r1 < r2;

      thus (F . r1) is open & (F . r2) is open & ( Cl (F . r1)) c= (F . r2)

      proof

        now

          per cases ;

            suppose

             A19: r1 in ( dyadic n) & r2 in ( dyadic n);

            then

             A20: (F . r1) = (G . r1) & (F . r2) = (G . r2) by A17;

            reconsider r1, r2 as Element of ( dyadic n) by A19;

            r1 < r2 by A18;

            hence thesis by A5, A20;

          end;

            suppose

             A21: r1 in ( dyadic n) & not r2 in ( dyadic n);

            then ((( axis r2) - 1) / (2 |^ (n + 1))) in ( dyadic n) & ((( axis r2) + 1) / (2 |^ (n + 1))) in ( dyadic n) by Th13;

            then

            consider q1,q2 be Element of ( dyadic n) such that

             A22: q1 = ((( axis r2) - 1) / (2 |^ (n + 1))) and

             A23: q2 = ((( axis r2) + 1) / (2 |^ (n + 1)));

            

             A24: r1 <= q1 by A18, A22, Th15;

            r2 in S by A21, XBOOLE_0:def 5;

            then

             A25: (D . r2) is Between of (G . q1), (G . q2) by A12, A22, A23;

            

             A26: q1 < q2 by A22, A23, Th12;

            then

             A27: (G . q2) is open & ( Cl (G . q1)) c= (G . q2) by A5;

            

             A28: (F . r2) = (D . r2) by A17, A21;

            

             A29: (G . q1) <> {} by A6;

            

             A30: (G . q1) is open by A5, A26;

            then

             A31: ( Cl (G . q1)) c= (F . r2) by A1, A28, A25, A29, A27, Def8;

            now

              per cases by A24, XXREAL_0: 1;

                suppose r1 = q1;

                hence thesis by A1, A17, A28, A25, A29, A30, A27, A31, Def8;

              end;

                suppose

                 A32: r1 < q1;

                

                 A33: (G . q1) c= ( Cl (G . q1)) by PRE_TOPC: 18;

                consider q0 be Element of ( dyadic n) such that

                 A34: q0 = r1 by A21;

                ( Cl (G . q0)) c= (G . q1) by A5, A32, A34;

                then ( Cl (F . r1)) c= (G . q1) by A17, A34;

                then

                 A35: ( Cl (F . r1)) c= ( Cl (G . q1)) by A33;

                

                 A36: (G . q0) is open by A5, A32, A34;

                

                 A37: (G . q1) is open by A5, A32, A34;

                then ( Cl (G . q1)) c= (F . r2) by A1, A28, A25, A29, A27, Def8;

                hence thesis by A1, A17, A28, A25, A29, A27, A34, A36, A37, A35, Def8;

              end;

            end;

            hence thesis;

          end;

            suppose

             A38: not r1 in ( dyadic n) & r2 in ( dyadic n);

            then ((( axis r1) - 1) / (2 |^ (n + 1))) in ( dyadic n) & ((( axis r1) + 1) / (2 |^ (n + 1))) in ( dyadic n) by Th13;

            then

            consider q1,q2 be Element of ( dyadic n) such that

             A39: q1 = ((( axis r1) - 1) / (2 |^ (n + 1))) and

             A40: q2 = ((( axis r1) + 1) / (2 |^ (n + 1)));

            

             A41: q2 <= r2 by A18, A40, Th15;

            r1 in S by A38, XBOOLE_0:def 5;

            then

             A42: (D . r1) is Between of (G . q1), (G . q2) by A12, A39, A40;

            

             A43: q1 < q2 by A39, A40, Th12;

            then

             A44: (G . q1) is open & ( Cl (G . q1)) c= (G . q2) by A5;

            

             A45: (F . r1) = (D . r1) by A17, A38;

            

             A46: (G . q1) <> {} by A6;

            

             A47: (G . q2) is open by A5, A43;

            then

             A48: ( Cl (F . r1)) c= (G . q2) by A1, A45, A42, A46, A44, Def8;

            now

              per cases by A41, XXREAL_0: 1;

                suppose q2 = r2;

                hence thesis by A1, A17, A45, A42, A46, A47, A44, A48, Def8;

              end;

                suppose

                 A49: q2 < r2;

                

                 A50: (G . q2) c= ( Cl (G . q2)) by PRE_TOPC: 18;

                consider q3 be Element of ( dyadic n) such that

                 A51: q3 = r2 by A38;

                

                 A52: (G . q2) is open by A5, A49, A51;

                then ( Cl (F . r1)) c= (G . q2) by A1, A45, A42, A46, A44, Def8;

                then

                 A53: ( Cl (F . r1)) c= ( Cl (G . q2)) by A50;

                ( Cl (G . q2)) c= (G . q3) by A5, A49, A51;

                then

                 A54: ( Cl (G . q2)) c= (F . r2) by A17, A51;

                (G . q3) is open by A5, A49, A51;

                hence thesis by A1, A17, A45, A42, A46, A44, A51, A52, A53, A54, Def8;

              end;

            end;

            hence thesis;

          end;

            suppose

             A55: not r1 in ( dyadic n) & not r2 in ( dyadic n);

            then ((( axis r1) - 1) / (2 |^ (n + 1))) in ( dyadic n) & ((( axis r1) + 1) / (2 |^ (n + 1))) in ( dyadic n) by Th13;

            then

            consider q11,q21 be Element of ( dyadic n) such that

             A56: q11 = ((( axis r1) - 1) / (2 |^ (n + 1))) and

             A57: q21 = ((( axis r1) + 1) / (2 |^ (n + 1)));

            r1 in S by A55, XBOOLE_0:def 5;

            then

             A58: (D . r1) is Between of (G . q11), (G . q21) by A12, A56, A57;

            

             A59: q11 < q21 by A56, A57, Th12;

            then

             A60: (G . q21) is open by A5;

            ((( axis r2) - 1) / (2 |^ (n + 1))) in ( dyadic n) & ((( axis r2) + 1) / (2 |^ (n + 1))) in ( dyadic n) by A55, Th13;

            then

            consider q12,q22 be Element of ( dyadic n) such that

             A61: q12 = ((( axis r2) - 1) / (2 |^ (n + 1))) and

             A62: q22 = ((( axis r2) + 1) / (2 |^ (n + 1)));

            r2 in S by A55, XBOOLE_0:def 5;

            then

             A63: (D . r2) is Between of (G . q12), (G . q22) by A12, A61, A62;

            

             A64: q12 < q22 by A61, A62, Th12;

            then

             A65: (G . q12) is open by A5;

            

             A66: (G . q22) is open & ( Cl (G . q12)) c= (G . q22) by A5, A64;

            

             A67: (G . q12) <> {} by A6;

            

             A68: (G . q11) <> {} by A6;

            

             A69: (F . r2) = (D . r2) by A17, A55;

            

             A70: (F . r1) = (D . r1) by A17, A55;

            

             A71: (G . q11) is open & ( Cl (G . q11)) c= (G . q21) by A5, A59;

            hence (F . r1) is open & (F . r2) is open by A1, A70, A58, A68, A60, A69, A63, A67, A65, A66, Def8;

            

             A72: q21 <= q12 by A18, A55, A57, A61, Th16;

            now

              per cases by A72, XXREAL_0: 1;

                suppose

                 A73: q21 = q12;

                ( Cl (F . r1)) c= (G . q21) & (G . q21) c= ( Cl (G . q21)) by A1, A70, A58, A68, A60, A71, Def8, PRE_TOPC: 18;

                then

                 A74: ( Cl (F . r1)) c= ( Cl (G . q21));

                ( Cl (G . q21)) c= (F . r2) by A1, A60, A69, A63, A67, A66, A73, Def8;

                hence ( Cl (F . r1)) c= (F . r2) by A74;

              end;

                suppose

                 A75: q21 < q12;

                ( Cl (F . r1)) c= (G . q21) & (G . q21) c= ( Cl (G . q21)) by A1, A70, A58, A68, A60, A71, Def8, PRE_TOPC: 18;

                then

                 A76: ( Cl (F . r1)) c= ( Cl (G . q21));

                ( Cl (G . q21)) c= (G . q12) by A5, A75;

                then

                 A77: ( Cl (F . r1)) c= (G . q12) by A76;

                (G . q12) c= ( Cl (G . q12)) & ( Cl (G . q12)) c= (F . r2) by A1, A69, A63, A67, A65, A66, Def8, PRE_TOPC: 18;

                then (G . q12) c= (F . r2);

                hence ( Cl (F . r1)) c= (F . r2) by A77;

              end;

            end;

            hence ( Cl (F . r1)) c= (F . r2);

          end;

        end;

        hence thesis;

      end;

      thus thesis by A17;

    end;