topdim_2.miz



    begin

    reserve n for Nat,

X for set,

Fx,Gx for Subset-Family of X;

    definition

      let X, Fx;

      :: TOPDIM_2:def1

      attr Fx is finite-order means

      : Def1: ex n st for Gx st Gx c= Fx & n in ( card Gx) holds ( meet Gx) is empty;

    end

    registration

      let X;

      cluster finite-order for Subset-Family of X;

      existence

      proof

        reconsider E = {} as Subset-Family of X by XBOOLE_1: 2;

        take E, 0 ;

        let G be Subset-Family of X;

        thus thesis;

      end;

      cluster finite -> finite-order for Subset-Family of X;

      coherence

      proof

        let F be Subset-Family of X;

        assume F is finite;

        then

        reconsider f = F as finite Subset-Family of X;

        take n = ( card f);

        let G be Subset-Family of X;

        assume that

         A1: G c= F and

         A2: n in ( card G);

        ( card G) c= ( Segm ( card f)) by A1, CARD_1: 11;

        hence ( meet G) is empty by A2, NAT_1: 44;

      end;

    end

    definition

      let X, Fx;

      :: TOPDIM_2:def2

      func order Fx -> ExtReal means

      : Def2: (for Gx st (it + 1) in ( card Gx) & Gx c= Fx holds ( meet Gx) is empty) & ex Gx st Gx c= Fx & ( card Gx) = (it + 1) & (( meet Gx) is non empty or Gx is empty) if Fx is finite-order

      otherwise it = +infty ;

      existence

      proof

        defpred P[ Nat] means for Gx st Gx c= Fx & $1 in ( card Gx) holds ( meet Gx) is empty;

        now

          assume Fx is finite-order;

          then

           A1: ex n st P[n];

          consider k be Nat such that

           A2: P[k] and

           A3: for n be Nat st P[n] holds k <= n from NAT_1:sch 5( A1);

          take O = (k - 1);

          thus for Gx st (O + 1) in ( card Gx) & Gx c= Fx holds ( meet Gx) is empty by A2;

          thus ex Gx be Subset-Family of X st Gx c= Fx & ( card Gx) = (O + 1) & (( meet Gx) is non empty or Gx is empty)

          proof

            per cases ;

              suppose

               A4: k = 0 ;

              reconsider E = {} as Subset-Family of X by XBOOLE_1: 2;

              take E;

              thus E c= Fx & ( card E) = (O + 1) & (( meet E) is non empty or E is empty) by A4;

            end;

              suppose k > 0 ;

              then

              reconsider k1 = (k - 1) as Element of NAT by NAT_1: 20;

              assume

               A5: for Gx st Gx c= Fx & ( card Gx) = (O + 1) holds ( meet Gx) is empty & Gx is non empty;

               P[k1]

              proof

                

                 A6: ( card ( Segm ( card (k1 + 1)))) = ( card (k1 + 1));

                

                 A7: ( card (k1 + 1)) = k;

                let Gx such that

                 A8: Gx c= Fx and

                 A9: k1 in ( card Gx);

                ( nextcard ( card ( Segm k1))) = ( card k) by A6, NAT_1: 42;

                then ( card k) c= ( card Gx) by A9, CARD_3: 90;

                then

                consider f be Function such that

                 A10: f is one-to-one & ( dom f) = k and

                 A11: ( rng f) c= Gx by CARD_1: 10;

                reconsider R = ( rng f) as Subset-Family of X by A11, XBOOLE_1: 1;

                (k,R) are_equipotent by A10, WELLORD2:def 4;

                then

                 A12: k = ( card R) by A7, CARD_1: 5;

                then

                 A13: R is non empty by A6;

                R c= Fx by A8, A11;

                then ( meet R) is empty by A5, A12;

                then ( meet Gx) c= {} by A11, A13, SETFAM_1: 6;

                hence thesis;

              end;

              then (k1 + 1) <= k1 by A3;

              hence contradiction by NAT_1: 13;

            end;

          end;

        end;

        hence thesis;

      end;

      uniqueness

      proof

        let O1,O2 be ExtReal;

        now

          assume Fx is finite-order;

          assume

           A14: for Gx st (O1 + 1) in ( card Gx) & Gx c= Fx holds ( meet Gx) is empty;

          given G1 be Subset-Family of X such that

           A15: G1 c= Fx and

           A16: ( card G1) = (O1 + 1) and

           A17: ( meet G1) is non empty or G1 is empty;

          assume

           A18: for Gx st (O2 + 1) in ( card Gx) & Gx c= Fx holds ( meet Gx) is empty;

          given G2 be Subset-Family of X such that

           A19: G2 c= Fx and

           A20: ( card G2) = (O2 + 1) and

           A21: ( meet G2) is non empty or G2 is empty;

           not ( card G2) in ( card G1) by A15, A17, A18, A20;

          then

           A22: ( card G1) c= ( card G2) by CARD_1: 3;

           not ( card G1) in ( card G2) by A14, A16, A19, A21;

          then ( card G1) = ( card G2) by A22, CARD_1: 3;

          hence O1 = O2 by A16, A20, XXREAL_3: 11;

        end;

        hence thesis;

      end;

      consistency ;

    end

    registration

      let X;

      let F be finite-order Subset-Family of X;

      cluster (( order F) + 1) -> natural;

      coherence

      proof

        consider G be Subset-Family of X such that

         A1: G c= F and

         A2: ( card G) = (( order F) + 1) and

         A3: ( meet G) is non empty or G is empty by Def2;

        consider n such that

         A4: for H be Subset-Family of X st H c= F & n in ( card H) holds ( meet H) is empty by Def1;

         not ( card n) in ( card G) by A1, A3, A4;

        then ( card G) c= n by CARD_1: 4;

        then

        reconsider G as finite Subset-Family of X;

        (( order F) + 1) = ((( card G) - 1) + 1) by A2;

        hence thesis;

      end;

      cluster ( order F) -> integer;

      coherence

      proof

        reconsider O1 = (( order F) + 1) as Nat by TARSKI: 1;

        (( order F) + 1) = ((O1 - 1) + 1);

        hence thesis by XXREAL_3: 11;

      end;

    end

    theorem :: TOPDIM_2:1

    

     Th1: ( order Fx) <= n implies Fx is finite-order

    proof

      assume ( order Fx) <= n;

      then ( order Fx) <> +infty by XXREAL_0: 4;

      hence thesis by Def2;

    end;

    theorem :: TOPDIM_2:2

    ( order Fx) <= n implies for Gx st Gx c= Fx & (n + 1) in ( card Gx) holds ( meet Gx) is empty

    proof

      

       A1: ( card (n + 1)) = (n + 1);

      assume

       A2: ( order Fx) <= n;

      then

      reconsider f = Fx as finite-order Subset-Family of X by Th1;

      (( order f) + 1) <= (n + 1) by A2, XREAL_1: 6;

      then (( order f) + 1) < ((n + 1) + 1) by NAT_1: 13;

      then

       A3: (( order f) + 1) in ( Segm (n + 2)) by NAT_1: 44;

      let Gx such that

       A4: Gx c= Fx and

       A5: (n + 1) in ( card Gx);

      ( nextcard ( Segm (n + 1))) c= ( card Gx) by A5, CARD_3: 90;

      then ( card ( Segm ((n + 1) + 1))) c= ( card Gx) by A1, NAT_1: 42;

      hence thesis by A4, A3, Def2;

    end;

    theorem :: TOPDIM_2:3

    

     Th3: (for G be finite Subset-Family of X st G c= Fx & (n + 1) < ( card G) holds ( meet G) is empty) implies ( order Fx) <= n

    proof

      set n1 = (n + 1);

      assume

       A1: for G be finite Subset-Family of X st G c= Fx & (n + 1) < ( card G) holds ( meet G) is empty;

       A2:

      now

        

         A3: ( card ( Segm (n1 + 1))) = (n1 + 1);

        let Gx such that

         A4: Gx c= Fx and

         A5: n1 in ( card Gx);

        ( nextcard ( card ( Segm n1))) = ( card (n1 + 1)) by A3, NAT_1: 42;

        then ( card (n1 + 1)) c= ( card Gx) by A5, CARD_3: 90;

        then

        consider f be Function such that

         A6: f is one-to-one & ( dom f) = (n1 + 1) and

         A7: ( rng f) c= Gx by CARD_1: 10;

        reconsider R = ( rng f) as Subset-Family of X by A7, XBOOLE_1: 1;

        ((n1 + 1),R) are_equipotent by A6, WELLORD2:def 4;

        then

         A8: (n1 + 1) = ( card R) by A3, CARD_1: 5;

        then

        reconsider R as finite Subset-Family of X;

        n1 < ( card R) by A8, NAT_1: 13;

        then

         A9: ( meet R) is empty by A1, A4, A7, XBOOLE_1: 1;

        R is non empty by A8;

        then ( meet Gx) c= {} by A7, A9, SETFAM_1: 6;

        hence ( meet Gx) is empty;

      end;

      then

      reconsider f = Fx as finite-order Subset-Family of X by Def1;

      consider Gx such that

       A10: Gx c= f and

       A11: ( card Gx) = (( order f) + 1) and

       A12: ( meet Gx) is non empty or Gx is empty by Def2;

      assume ( order Fx) > n;

      then (( order f) + 1) > n1 by XREAL_1: 6;

      then n1 in ( Segm (( order f) + 1)) by NAT_1: 44;

      hence thesis by A2, A10, A12, A11;

    end;

    begin

    reserve TM for metrizable TopSpace,

TM1,TM2 for finite-ind second-countable metrizable TopSpace,

A,B,L,H for Subset of TM,

U,W for open Subset of TM,

p for Point of TM,

F,G for finite Subset-Family of TM,

I for Integer;

    

     Lm1: for T be TopSpace, Af be finite-ind Subset of T holds (( ind Af) + 1) is Nat

    proof

      let T be TopSpace, Af be finite-ind Subset of T;

      Af in (( Seq_of_ind T) . (1 + ( ind Af))) by TOPDIM_1:def 5;

      then (( ind Af) + 1) in ( dom ( Seq_of_ind T)) by FUNCT_1:def 2;

      hence thesis;

    end;

    

     Lm2: for T be TopSpace, g be SetSequence of T st for i be Nat holds (g . i) is finite-ind & ( ind (g . i)) <= n & (g . i) is F_sigma holds ex G be Subset-Family of T st G is closed & G is finite-ind & ( ind G) <= n & G is countable & ( Union g) = ( union G)

    proof

      let T be TopSpace;

      let g be SetSequence of T such that

       A1: for i be Nat holds (g . i) is finite-ind & ( ind (g . i)) <= n & (g . i) is F_sigma;

      defpred F[ object, object] means for n be Nat, F be Subset-Family of T st n = $1 & F = $2 holds ( union F) = (g . n) & F is closed countable;

      

       A2: for x be object st x in NAT holds ex y be object st y in ( bool ( bool the carrier of T)) & F[x, y]

      proof

        let x be object;

        assume x in NAT ;

        then

        reconsider n = x as Element of NAT ;

        (g . n) is F_sigma by A1;

        then

        consider y be closed countable Subset-Family of T such that

         A3: (g . n) = ( union y) by TOPGEN_4:def 6;

        take y;

        thus thesis by A3;

      end;

      consider f be SetSequence of ( bool the carrier of T) qua set such that

       A4: for x be object st x in NAT holds F[x, (f . x)] from FUNCT_2:sch 1( A2);

      take F = ( Union f);

      thus F is closed

      proof

        let A be Subset of T;

        assume A in F;

        then

        consider n be Nat such that

         A5: A in (f . n) by PROB_1: 12;

        n in NAT by ORDINAL1:def 12;

        then (f . n) is closed by A4;

        hence thesis by A5;

      end;

      for A be Subset of T st A in F holds A is finite-ind & ( ind A) <= n

      proof

        let A be Subset of T;

        assume A in F;

        then

        consider i be Nat such that

         A6: A in (f . i) by PROB_1: 12;

        i in NAT by ORDINAL1:def 12;

        then ( union (f . i)) = (g . i) by A4;

        then

         A7: A c= (g . i) by A6, ZFMISC_1: 74;

        

         A8: ( ind (g . i)) <= n by A1;

        

         A9: (g . i) is finite-ind by A1;

        then ( ind A) <= ( ind (g . i)) by A7, TOPDIM_1: 19;

        hence thesis by A7, A8, A9, TOPDIM_1: 19, XXREAL_0: 2;

      end;

      hence F is finite-ind & ( ind F) <= n by TOPDIM_1: 11;

      for x be set st x in ( dom f) holds (f . x) is countable by A4;

      hence F is countable by CARD_4: 11;

      thus ( Union g) c= ( union F)

      proof

        let x be object;

        assume x in ( Union g);

        then

        consider i be Nat such that

         A10: x in (g . i) by PROB_1: 12;

        i in NAT by ORDINAL1:def 12;

        then ( union (f . i)) = (g . i) by A4;

        then

        consider y be set such that

         A11: x in y and

         A12: y in (f . i) by A10, TARSKI:def 4;

        y in F by A12, PROB_1: 12;

        hence thesis by A11, TARSKI:def 4;

      end;

      thus ( union F) c= ( Union g)

      proof

        let x be object;

        assume x in ( union F);

        then

        consider y be set such that

         A13: x in y and

         A14: y in F by TARSKI:def 4;

        consider i be Nat such that

         A15: y in (f . i) by A14, PROB_1: 12;

        i in NAT by ORDINAL1:def 12;

        then ( union (f . i)) = (g . i) by A4;

        then x in (g . i) by A13, A15, TARSKI:def 4;

        hence thesis by PROB_1: 12;

      end;

    end;

    

     Lm3: for T be metrizable TopSpace st T is second-countable holds ((ex F be Subset-Family of T st F is closed & F is Cover of T & F is countable & F is finite-ind & ( ind F) <= n) implies T is finite-ind & ( ind T) <= n) & (T is finite-ind & ( ind T) <= n implies ex A,B be Subset of T st ( [#] T) = (A \/ B) & A misses B & ( ind A) <= (n - 1) & ( ind B) <= 0 )

    proof

      defpred R[ Nat] means for T be metrizable TopSpace st T is second-countable & T is finite-ind & ( ind T) <= $1 holds ex A,B be Subset of T st ( [#] T) = (A \/ B) & A misses B & ( ind A) <= ($1 - 1) & ( ind B) <= 0 ;

      defpred P[ Nat] means for T be metrizable TopSpace st T is second-countable & ex F be Subset-Family of T st F is closed & F is Cover of T & F is countable & F is finite-ind & ( ind F) <= $1 holds T is finite-ind & ( ind T) <= $1;

      

       A1: for n st P[n] holds R[(n + 1)]

      proof

        defpred P1[ set] means not contradiction;

        let n such that

         A2: P[n];

        let T be metrizable TopSpace such that

         A3: T is second-countable and

         A4: T is finite-ind and

         A5: ( ind T) <= (n + 1);

        consider B be Basis of T such that

         A6: for A be Subset of T st A in B holds ( Fr A) is finite-ind & ( ind ( Fr A)) <= ((n + 1) - 1) by A4, A5, TOPDIM_1: 31;

        deffunc F( Subset of T) = ( Fr $1);

        consider uB be Basis of T such that

         A7: uB c= B and

         A8: uB is countable by A3, METRIZTS: 24;

        defpred P[ set] means $1 in uB & P1[$1];

        consider S be Subset-Family of T such that

         A9: S = { F(b) where b be Subset of T : P[b] } from LMOD_7:sch 5;

        set uS = ( union S);

        set TS = (T | uS);

        

         A10: ( [#] TS) = uS by PRE_TOPC:def 5;

        then

        reconsider S9 = S as Subset-Family of TS by ZFMISC_1: 82;

        

         A11: (T | (uS ` )) is second-countable by A3;

        for a be Subset of TS st a in S9 holds a is finite-ind & ( ind a) <= n

        proof

          let a be Subset of TS;

          assume a in S9;

          then

          consider b be Subset of T such that

           A12: a = F(b) and

           A13: P[b] by A9;

          ( Fr b) is finite-ind & ( ind ( Fr b)) <= ((n + 1) - 1) by A6, A7, A13;

          hence thesis by A12, TOPDIM_1: 21;

        end;

        then

         A14: S9 is finite-ind & ( ind S9) <= n by TOPDIM_1: 11;

        

         A15: for p be Point of T, U be open Subset of T st p in U holds ex W be open Subset of T st p in W & W c= U & (uS ` ) misses ( Fr W)

        proof

          let p be Point of T, U be open Subset of T;

          assume p in U;

          then

          consider a be Subset of T such that

           A16: a in uB and

           A17: p in a & a c= U by YELLOW_9: 31;

          uB c= the topology of T by TOPS_2: 64;

          then

          reconsider a as open Subset of T by A16, PRE_TOPC:def 2;

          take a;

           F(a) in S by A9, A16;

          then F(a) c= uS by ZFMISC_1: 74;

          hence thesis by A17, SUBSET_1: 24;

        end;

        take uS, (uS ` );

        

         A18: ( card { F(b) where b be Subset of T : b in uB & P1[b] }) c= ( card uB) from BORSUK_2:sch 1;

        ( card uB) c= omega by A8;

        then ( card S) c= omega by A9, A18;

        then

         A19: S9 is countable;

        

         A20: S9 is closed

        proof

          let a be Subset of TS;

          assume a in S9;

          then ex b be Subset of T st a = F(b) & P[b] by A9;

          hence thesis by TSEP_1: 8;

        end;

        S9 is Cover of TS by A10, SETFAM_1:def 11;

        then ( ind TS) <= n by A2, A3, A14, A19, A20;

        hence thesis by A4, A11, A15, PRE_TOPC: 2, SUBSET_1: 23, TOPDIM_1: 17, TOPDIM_1: 38;

      end;

      

       A21: P[ 0 ] by TOPDIM_1: 36;

      

       A22: for n st P[n] holds P[(n + 1)]

      proof

        let n such that

         A23: P[n];

        let T be metrizable TopSpace such that

         A24: T is second-countable;

        given F be Subset-Family of T such that

         A25: F is closed and

         A26: F is Cover of T and

         A27: F is countable and

         A28: F is finite-ind & ( ind F) <= (n + 1);

        per cases ;

          suppose T is empty;

          hence thesis by TOPDIM_1: 6;

        end;

          suppose

           A29: T is non empty;

          set cT = the carrier of T;

          

           A30: F is non empty by A26, A29, SETFAM_1: 45, ZFMISC_1: 2;

          then

          consider f be sequence of F such that

           A31: ( rng f) = F by A27, CARD_3: 96;

          ( dom f) = NAT by A30, FUNCT_2:def 1;

          then

          reconsider f as SetSequence of T by A31, FUNCT_2: 2;

          consider g be SetSequence of T such that

           A32: ( union ( rng f)) = ( union ( rng g)) and

           A33: for i,j be Nat st i <> j holds (g . i) misses (g . j) and

           A34: for n holds ex fn be finite Subset-Family of T st fn = { (f . i) where i be Element of NAT : i < n } & (g . n) = ((f . n) \ ( union fn)) by TOPDIM_1: 33;

          defpred Q[ object, object] means for i be Nat, A,B be Subset of T st $1 = i & $2 = [A, B] holds (A \/ B) = (g . i) & A is finite-ind & B is finite-ind & ( ind A) <= n & ( ind B) <= 0 ;

          

           A35: for x be object st x in NAT holds ex y be object st y in [:( bool cT), ( bool cT):] & Q[x, y]

          proof

            let x be object;

            assume x in NAT ;

            then

            reconsider N = x as Element of NAT ;

            reconsider gN = (g . N) as Subset of T;

            ( dom f) = NAT by FUNCT_2:def 1;

            then

             A36: (f . N) in F by A31, FUNCT_1:def 3;

            then

             A37: (f . N) is finite-ind by A28;

            ex fn be finite Subset-Family of T st fn = { (f . i) where i be Element of NAT : i < N } & (g . N) = ((f . N) \ ( union fn)) by A34;

            then

             A38: (g . N) c= (f . N) by XBOOLE_1: 36;

            then

             A39: (g . N) is finite-ind by A37, TOPDIM_1: 19;

            

             A40: ( ind (g . N)) <= ( ind (f . N)) by A37, A38, TOPDIM_1: 19;

            ( ind (f . N)) <= (n + 1) by A28, A36, TOPDIM_1: 11;

            then

             A41: ( ind (g . N)) <= (n + 1) by A40, XXREAL_0: 2;

            ( ind (T | gN)) = ( ind gN) by A39, TOPDIM_1: 17;

            then

            consider A,B be Subset of (T | gN) such that

             A42: (A \/ B) = ( [#] (T | gN)) and A misses B and

             A43: ( ind A) <= ((n + 1) - 1) & ( ind B) <= 0 by A1, A23, A24, A39, A41;

            

             A44: A is finite-ind by A39;

            ( [#] (T | gN)) = gN by PRE_TOPC:def 5;

            then

            reconsider A9 = A, B9 = B as Subset of T by XBOOLE_1: 1;

            B is finite-ind by A39;

            then

             A45: B9 is finite-ind & ( ind B9) = ( ind B) by TOPDIM_1: 22;

            take y = [A9, B9];

            thus y in [:( bool cT), ( bool cT):];

            let i be Nat, a,b be Subset of T such that

             A46: x = i and

             A47: y = [a, b];

            

             A48: a = A9 by A47, XTUPLE_0: 1;

            (A9 \/ B9) = (g . i) by A42, A46, PRE_TOPC:def 5;

            hence thesis by A43, A44, A45, A47, A48, TOPDIM_1: 22, XTUPLE_0: 1;

          end;

          consider P12 be sequence of [:( bool cT), ( bool cT):] such that

           A49: for x be object st x in NAT holds Q[x, (P12 . x)] from FUNCT_2:sch 1( A35);

          set P1 = ( pr1 P12), P2 = ( pr2 P12);

          set U1 = ( Union P1), U2 = ( Union P2);

          set Tu1 = (T | U1), Tu2 = (T | U2);

          reconsider Tu1 as metrizable TopSpace;

          

           A50: ( dom P1) = NAT by FUNCT_2:def 1;

          

           A51: ( [#] Tu1) = U1 by PRE_TOPC:def 5;

          then

          reconsider P1 as SetSequence of Tu1 by A50, FUNCT_2: 2, ZFMISC_1: 82;

          reconsider Tu2 as metrizable TopSpace;

          

           A52: ( dom P2) = NAT by FUNCT_2:def 1;

          

           A53: for i be Nat holds (g . i) is F_sigma

          proof

            let i be Nat;

            consider fi be finite Subset-Family of T such that

             A54: fi = { (f . j) where j be Element of NAT : j < i } and

             A55: (g . i) = ((f . i) \ ( union fi)) by A34;

            fi is closed

            proof

              let A be Subset of T;

              assume A in fi;

              then

               A56: ex j be Element of NAT st A = (f . j) & j < i by A54;

              ( dom f) = NAT by FUNCT_2:def 1;

              then A in F by A31, A56, FUNCT_1:def 3;

              hence thesis by A25;

            end;

            then

             A57: ( union fi) is closed by TOPS_2: 21;

            ( dom f) = NAT & i in NAT by FUNCT_2:def 1, ORDINAL1:def 12;

            then (f . i) in F by A31, FUNCT_1:def 3;

            then (f . i) is closed by A25;

            then

             A58: (f . i) is F_sigma by A29, TOPGEN_4: 43;

            ((( union fi) ` ) /\ (f . i)) = ((( [#] T) /\ (f . i)) \ ( union fi)) by XBOOLE_1: 49

            .= (g . i) by A55, XBOOLE_1: 28;

            hence thesis by A29, A57, A58, TOPGEN_4: 39;

          end;

          for i be Nat holds (P1 . i) is finite-ind & ( ind (P1 . i)) <= n & (P1 . i) is F_sigma

          proof

            let i be Nat;

            consider y1,y2 be object such that

             A59: y1 in ( bool cT) and

             A60: y2 in ( bool cT) and

             A61: (P12 . i) = [y1, y2] by ZFMISC_1:def 2;

            reconsider y1 as Subset of T by A59;

            reconsider y2 as set by TARSKI: 1;

            

             A62: i in NAT by ORDINAL1:def 12;

            then

             A63: y1 is finite-ind & ( ind y1) <= n by A49, A60, A61;

            ( [y1, y2] `1 ) = y1 & ( dom P12) = NAT by FUNCT_2:def 1;

            then

             A64: y1 = (P1 . i) by A61, A62, MCART_1:def 12;

            

             A65: (U1 /\ (g . i)) c= (P1 . i)

            proof

              let x be object;

              assume

               A66: x in (U1 /\ (g . i));

              then

               A67: x in (g . i) by XBOOLE_0:def 4;

              x in U1 by A66, XBOOLE_0:def 4;

              then

              consider j be Nat such that

               A68: x in (P1 . j) by PROB_1: 12;

              consider z1,z2 be object such that

               A69: z1 in ( bool cT) & z2 in ( bool cT) and

               A70: (P12 . j) = [z1, z2] by ZFMISC_1:def 2;

              

               A71: j in NAT by ORDINAL1:def 12;

              reconsider z1, z2 as set by TARSKI: 1;

              ( [z1, z2] `1 ) = z1 & ( dom P12) = NAT by FUNCT_2:def 1;

              then

               A72: z1 = (P1 . j) by A70, MCART_1:def 12, A71;

              (z1 \/ z2) = (g . j) by A49, A69, A70, A71;

              then x in (g . j) by A68, A72, XBOOLE_0:def 3;

              then (g . i) meets (g . j) by A67, XBOOLE_0: 3;

              hence thesis by A33, A68;

            end;

            (y1 \/ y2) = (g . i) by A49, A60, A61, A62;

            then (P1 . i) c= (g . i) by A64, XBOOLE_1: 7;

            then (P1 . i) c= (U1 /\ (g . i)) by A51, XBOOLE_1: 19;

            then (P1 . i) = (U1 /\ (g . i)) & (g . i) is F_sigma by A53, A65;

            hence thesis by A63, A64, METRIZTS: 10, TOPDIM_1: 21;

          end;

          then

          consider G1 be Subset-Family of Tu1 such that

           A73: G1 is closed & G1 is finite-ind & ( ind G1) <= n & G1 is countable and

           A74: ( Union P1) = ( union G1) by Lm2;

          

           A75: G1 is Cover of Tu1 by A51, A74, SETFAM_1:def 11;

          then

           A76: Tu1 is finite-ind by A23, A24, A73;

          then

           A77: U1 is finite-ind by TOPDIM_1: 18;

          

           A78: ( [#] Tu2) = U2 by PRE_TOPC:def 5;

          then

          reconsider P2 as SetSequence of Tu2 by A52, FUNCT_2: 2, ZFMISC_1: 82;

          for i be Nat holds (P2 . i) is finite-ind & ( ind (P2 . i)) <= 0 & (P2 . i) is F_sigma

          proof

            let i be Nat;

            consider y1,y2 be object such that

             A79: y1 in ( bool cT) and

             A80: y2 in ( bool cT) and

             A81: (P12 . i) = [y1, y2] by ZFMISC_1:def 2;

            reconsider y2 as Subset of T by A80;

            reconsider y1 as set by TARSKI: 1;

            

             A82: i in NAT by ORDINAL1:def 12;

            then

             A83: y2 is finite-ind & ( ind y2) <= 0 by A49, A79, A81;

            ( [y1, y2] `2 ) = y2 & ( dom P12) = NAT by FUNCT_2:def 1;

            then

             A84: y2 = (P2 . i) by A81, A82, MCART_1:def 13;

            

             A85: (U2 /\ (g . i)) c= (P2 . i)

            proof

              let x be object;

              assume

               A86: x in (U2 /\ (g . i));

              then

               A87: x in (g . i) by XBOOLE_0:def 4;

              x in U2 by A86, XBOOLE_0:def 4;

              then

              consider j be Nat such that

               A88: x in (P2 . j) by PROB_1: 12;

              consider z1,z2 be object such that

               A89: z1 in ( bool cT) & z2 in ( bool cT) and

               A90: (P12 . j) = [z1, z2] by ZFMISC_1:def 2;

              

               A91: j in NAT by ORDINAL1:def 12;

              reconsider z1, z2 as set by TARSKI: 1;

              ( [z1, z2] `2 ) = z2 & ( dom P12) = NAT by FUNCT_2:def 1;

              then

               A92: z2 = (P2 . j) by A90, MCART_1:def 13, A91;

              (z1 \/ z2) = (g . j) by A49, A89, A90, A91;

              then x in (g . j) by A88, A92, XBOOLE_0:def 3;

              then (g . i) meets (g . j) by A87, XBOOLE_0: 3;

              hence thesis by A33, A88;

            end;

            (y1 \/ y2) = (g . i) by A49, A79, A81, A82;

            then (P2 . i) c= (g . i) by A84, XBOOLE_1: 7;

            then (P2 . i) c= (U2 /\ (g . i)) by A78, XBOOLE_1: 19;

            then (P2 . i) = (U2 /\ (g . i)) & (g . i) is F_sigma by A53, A85;

            hence thesis by A83, A84, METRIZTS: 10, TOPDIM_1: 21;

          end;

          then

          consider G2 be Subset-Family of Tu2 such that

           A93: G2 is closed & G2 is finite-ind & ( ind G2) <= 0 & G2 is countable and

           A94: ( Union P2) = ( union G2) by Lm2;

          

           A95: G2 is Cover of Tu2 by A78, A94, SETFAM_1:def 11;

          then Tu2 is finite-ind by A23, A24, A93;

          then

           A96: U2 is finite-ind by TOPDIM_1: 18;

          ( ind Tu1) <= n by A23, A24, A73, A75;

          then ( ind U1) <= n by A77, TOPDIM_1: 17;

          then

           A97: (( ind U1) + 1) <= (n + 1) by XREAL_1: 6;

          

           A98: U1 is finite-ind by A76, TOPDIM_1: 18;

          ( [#] T) c= (U1 \/ U2)

          proof

            let x be object;

            

             A99: ( dom P12) = NAT by FUNCT_2:def 1;

            assume x in ( [#] T);

            then x in ( Union g) by A26, A31, A32, SETFAM_1: 45;

            then

            consider i be Nat such that

             A100: x in (g . i) by PROB_1: 12;

            consider y1,y2 be object such that

             A101: y1 in ( bool cT) & y2 in ( bool cT) and

             A102: (P12 . i) = [y1, y2] by ZFMISC_1:def 2;

            reconsider y1, y2 as set by TARSKI: 1;

            

             A103: i in NAT by ORDINAL1:def 12;

            ( [y1, y2] `1 ) = y1;

            then

             A104: y1 = (P1 . i) by A99, A102, MCART_1:def 12, A103;

            ( [y1, y2] `2 ) = y2;

            then

             A105: y2 = (P2 . i) by A99, A102, MCART_1:def 13, A103;

            (y1 \/ y2) = (g . i) by A49, A101, A102, A103;

            then x in (P1 . i) or x in (P2 . i) by A100, A104, A105, XBOOLE_0:def 3;

            then x in U1 or x in U2 by PROB_1: 12;

            hence thesis by XBOOLE_0:def 3;

          end;

          then

           A106: (U1 \/ U2) = ( [#] T);

          ( ind Tu2) <= 0 by A24, A93, A95, TOPDIM_1: 36;

          then

           A107: ( ind U2) <= 0 by A96, TOPDIM_1: 17;

          (T | U2) is second-countable by A24;

          then (U1 \/ U2) is finite-ind & ( ind (U1 \/ U2)) <= (( ind U1) + 1) by A96, A107, A98, TOPDIM_1: 40;

          hence thesis by A106, A97, XXREAL_0: 2;

        end;

      end;

      

       A108: for n holds P[n] from NAT_1:sch 2( A21, A22);

      let T be metrizable TopSpace such that

       A109: T is second-countable;

      thus (ex F be Subset-Family of T st F is closed & F is Cover of T & F is countable & F is finite-ind & ( ind F) <= n) implies T is finite-ind & ( ind T) <= n by A108, A109;

      assume that

       A110: T is finite-ind and

       A111: ( ind T) <= n;

      per cases ;

        suppose

         A112: n = 0 ;

        take ( {} T), ( [#] T);

        thus thesis by A111, A112, TOPDIM_1: 6;

      end;

        suppose n > 0 ;

        then

        reconsider n1 = (n - 1) as Element of NAT by NAT_1: 20;

         P[n1] & (n1 + 1) = n by A108;

        hence thesis by A1, A109, A110, A111;

      end;

    end;

    theorem :: TOPDIM_2:4

    for TM st TM is second-countable & ex F st F is closed & F is Cover of TM & F is countable & F is finite-ind & ( ind F) <= n holds TM is finite-ind & ( ind TM) <= n by Lm3;

    theorem :: TOPDIM_2:5

    

     Th5: for A,B be finite-ind Subset of TM st A is closed & (TM | (A \/ B)) is second-countable & ( ind A) <= I & ( ind B) <= I holds ( ind (A \/ B)) <= I & (A \/ B) is finite-ind

    proof

      let A,B be finite-ind Subset of TM such that

       A1: A is closed and

       A2: (TM | (A \/ B)) is second-countable and

       A3: ( ind A) <= I and

       A4: ( ind B) <= I;

      ( - 1) <= ( ind A) by TOPDIM_1: 5;

      then

       A5: ( - 1) <= I by A3, XXREAL_0: 2;

      per cases ;

        suppose (A \/ B) is empty;

        hence thesis by A5, TOPDIM_1: 6;

      end;

        suppose

         A6: (A \/ B) is non empty;

        then

         A7: TM is non empty;

        A is non empty or B is non empty by A6;

        then 0 <= ( ind A) or 0 <= ( ind B) by A7;

        then

         A8: I in NAT by A3, A4, INT_1: 3;

        reconsider AB = (A \/ B) as Subset of TM;

        set Tab = (TM | AB);

        

         A9: ( [#] Tab) = AB by PRE_TOPC:def 5;

        then

        reconsider a = A, b = B as Subset of Tab by XBOOLE_1: 7;

        (A /\ ( [#] Tab)) = a by XBOOLE_1: 28;

        then

         A10: a is closed by A1, TSP_1:def 2;

        then

        consider F be closed countable Subset-Family of Tab such that

         A11: (a ` ) = ( union F) by TOPGEN_4:def 6;

        reconsider a, b as finite-ind Subset of Tab by TOPDIM_1: 21;

        reconsider AA = {a} as Subset-Family of Tab;

        ( union (AA \/ F)) = (( union AA) \/ ( union F)) by ZFMISC_1: 78

        .= (a \/ (a ` )) by A11, ZFMISC_1: 25

        .= ( [#] Tab) by PRE_TOPC: 2;

        then

         A12: (AA \/ F) is Cover of Tab by SETFAM_1:def 11;

        AA is closed by A10, TARSKI:def 1;

        then

         A13: (AA \/ F) is closed by TOPS_2: 16;

        for D be Subset of Tab st D in (AA \/ F) holds D is finite-ind & ( ind D) <= I

        proof

          let D be Subset of Tab such that

           A14: D in (AA \/ F);

          per cases by A14, XBOOLE_0:def 3;

            suppose D in AA;

            then D = a by TARSKI:def 1;

            hence thesis by A3, TOPDIM_1: 21;

          end;

            suppose

             A15: D in F;

            (a ` ) = (b \ a) by A9, XBOOLE_1: 40;

            then

             A16: (a ` ) c= b by XBOOLE_1: 36;

            D c= (a ` ) by A11, A15, ZFMISC_1: 74;

            then

             A17: D c= b by A16;

            then ( ind b) = ( ind B) & ( ind D) <= ( ind b) by TOPDIM_1: 19, TOPDIM_1: 21;

            hence thesis by A4, A17, TOPDIM_1: 19, XXREAL_0: 2;

          end;

        end;

        then

         A18: (AA \/ F) is finite-ind & ( ind (AA \/ F)) <= I by A5, TOPDIM_1: 11;

        

         A19: (AA \/ F) is countable by CARD_2: 85;

        then Tab is finite-ind by A2, A8, A12, A13, A18, Lm3;

        then

         A20: (A \/ B) is finite-ind by TOPDIM_1: 18;

        ( ind Tab) <= I by A2, A8, A12, A13, A18, A19, Lm3;

        hence thesis by A20, TOPDIM_1: 17;

      end;

    end;

    theorem :: TOPDIM_2:6

    for TM st TM is second-countable & TM is finite-ind & ( ind TM) <= n holds ex A, B st ( [#] TM) = (A \/ B) & A misses B & ( ind A) <= (n - 1) & ( ind B) <= 0 by Lm3;

    theorem :: TOPDIM_2:7

    

     Th7: for TM st TM is second-countable finite-ind & ( ind TM) <= I holds ex F st F is Cover of TM & F is finite-ind & ( ind F) <= 0 & ( card F) <= (I + 1) & for A, B st A in F & B in F & A meets B holds A = B

    proof

      defpred P[ Nat] means for TM st TM is second-countable finite-ind & ( ind TM) <= ($1 - 1) holds ex F be finite Subset-Family of TM st F is Cover of TM & F is finite-ind & ( ind F) <= 0 & ( card F) <= $1 & for A,B be Subset of TM st A in F & B in F & A meets B holds A = B;

      let TM such that

       A1: TM is second-countable finite-ind and

       A2: ( ind TM) <= I;

      ( - 1) <= ( ind ( [#] TM)) by A1, TOPDIM_1: 5;

      then ( - 1) <= I by A2, XXREAL_0: 2;

      then (( - 1) + 1) <= (I + 1) by XREAL_1: 6;

      then

      reconsider i1 = (I + 1) as Element of NAT by INT_1: 3;

      

       A3: for n st P[n] holds P[(n + 1)]

      proof

        let n such that

         A4: P[n];

        let TM such that

         A5: TM is second-countable and

         A6: TM is finite-ind and

         A7: ( ind TM) <= ((n + 1) - 1);

        consider A,B be Subset of TM such that

         A8: ( [#] TM) = (A \/ B) and

         A9: A misses B and

         A10: ( ind A) <= (n - 1) and

         A11: ( ind B) <= 0 by A5, A6, A7, Lm3;

        set BB = {B};

        for b be Subset of TM st b in BB holds b is finite-ind & ( ind b) <= 0 by A6, A11, TARSKI:def 1;

        then

         A12: BB is finite-ind & ( ind BB) <= 0 by TOPDIM_1: 11;

        set TA = (TM | A);

        ( ind TA) = ( ind A) by A6, TOPDIM_1: 17;

        then

        consider F be finite Subset-Family of TA such that

         A13: F is Cover of TA and

         A14: F is finite-ind and

         A15: ( ind F) <= 0 and

         A16: ( card F) <= n and

         A17: for A,B be Subset of TA st A in F & B in F & A meets B holds A = B by A4, A5, A6, A10;

        ( [#] TA) c= ( [#] TM) by PRE_TOPC:def 4;

        then ( bool ( [#] TA)) c= ( bool ( [#] TM)) by ZFMISC_1: 67;

        then

        reconsider F9 = F as finite Subset-Family of TM by XBOOLE_1: 1;

        take G = (F9 \/ BB);

        

         A18: ( union F9) = ( [#] TA) by A13, SETFAM_1: 45

        .= A by PRE_TOPC:def 5;

        

        then ( union G) = (A \/ ( union BB)) by ZFMISC_1: 78

        .= ( [#] TM) by A8, ZFMISC_1: 25;

        hence G is Cover of TM by SETFAM_1:def 11;

        F9 is finite-ind & ( ind F9) = ( ind F) by A14, TOPDIM_1: 29;

        hence G is finite-ind & ( ind G) <= 0 by A12, A15, TOPDIM_1: 13;

        ( card BB) = 1 by CARD_1: 30;

        then

         A19: ( card G) <= (( card F9) + 1) by CARD_2: 43;

        (( card F9) + 1) <= (n + 1) by A16, XREAL_1: 6;

        hence ( card G) <= (n + 1) by A19, XXREAL_0: 2;

        let a,b be Subset of TM such that

         A20: a in G & b in G and

         A21: a meets b;

        per cases by A20, XBOOLE_0:def 3;

          suppose a in F & b in F;

          hence thesis by A17, A21;

        end;

          suppose

           A22: a in F & b in BB;

          then b = B by TARSKI:def 1;

          hence thesis by A9, A18, A21, A22, XBOOLE_1: 63, ZFMISC_1: 74;

        end;

          suppose

           A23: a in BB & b in F;

          then a = B by TARSKI:def 1;

          hence thesis by A9, A18, A21, A23, XBOOLE_1: 63, ZFMISC_1: 74;

        end;

          suppose

           A24: a in BB & b in BB;

          then a = B by TARSKI:def 1;

          hence thesis by A24, TARSKI:def 1;

        end;

      end;

      

       A25: P[ 0 ]

      proof

        let TM such that TM is second-countable and

         A26: TM is finite-ind and

         A27: ( ind TM) <= ( 0 - 1);

        ( ind ( [#] TM)) >= ( - 1) by A26, TOPDIM_1: 5;

        then ( ind ( [#] TM)) = ( - 1) by A27, XXREAL_0: 1;

        then

         A28: ( [#] TM) = ( {} TM) by A26, TOPDIM_1: 6;

        reconsider F = {} as empty Subset-Family of TM by TOPGEN_4: 18;

        take F;

        F c= {( {} TM)};

        hence thesis by A28, SETFAM_1:def 11, TOPDIM_1: 10, ZFMISC_1: 2;

      end;

      for n holds P[n] from NAT_1:sch 2( A25, A3);

      then P[i1];

      hence thesis by A1, A2;

    end;

    theorem :: TOPDIM_2:8

    

     Th8: for TM st TM is second-countable & ex F st F is Cover of TM & F is finite-ind & ( ind F) <= 0 & ( card F) <= (I + 1) holds TM is finite-ind & ( ind TM) <= I

    proof

      defpred P[ Nat] means for TM st TM is second-countable & ex F be finite Subset-Family of TM st F is Cover of TM & F is finite-ind & ( ind F) <= 0 & ( card F) <= $1 holds TM is finite-ind & ( ind TM) <= ($1 - 1);

      let TM such that

       A1: TM is second-countable;

      given F be finite Subset-Family of TM such that

       A2: F is Cover of TM & F is finite-ind & ( ind F) <= 0 and

       A3: ( card F) <= (I + 1);

      reconsider i1 = (I + 1) as Element of NAT by A3, INT_1: 3;

      

       A4: P[ 0 ]

      proof

        let TM such that TM is second-countable;

        given F be finite Subset-Family of TM such that

         A5: F is Cover of TM and F is finite-ind and ( ind F) <= 0 and

         A6: ( card F) <= 0 ;

        F = {} by A6;

        then ( [#] TM) = {} by A5, SETFAM_1: 45, ZFMISC_1: 2;

        hence thesis by TOPDIM_1: 6;

      end;

      

       A7: for n st P[n] holds P[(n + 1)]

      proof

        let n such that

         A8: P[n];

        let TM such that

         A9: TM is second-countable;

        given F be finite Subset-Family of TM such that

         A10: F is Cover of TM and

         A11: F is finite-ind and

         A12: ( ind F) <= 0 and

         A13: ( card F) <= (n + 1);

        per cases ;

          suppose F = {} ;

          then ( card F) = 0 ;

          hence thesis by A4, A9, A10, A11, A12;

        end;

          suppose F <> {} ;

          then

          consider A be object such that

           A14: A in F by XBOOLE_0:def 1;

          reconsider A as Subset of TM by A14;

          set AA = {A};

          set FA = (F \ AA);

          

           A15: (FA \/ AA) = F by A14, ZFMISC_1: 116;

          

           A16: ( [#] TM) = ( union F) by A10, SETFAM_1: 45

          .= (( union FA) \/ ( union AA)) by A15, ZFMISC_1: 78

          .= (( union FA) \/ A) by ZFMISC_1: 25;

          

           A17: FA c= F by XBOOLE_1: 36;

          then

           A18: ( ind FA) <= 0 by A11, A12, TOPDIM_1: 12;

           not A in FA by ZFMISC_1: 56;

          then FA c< F by A14, A17;

          then ( card FA) < (n + 1) by A13, CARD_2: 48, XXREAL_0: 2;

          then

           A19: ( card FA) <= n by NAT_1: 13;

          reconsider uFA = ( union FA) as Subset of TM;

          set Tu = (TM | uFA);

          

           A20: ( [#] Tu) = uFA by PRE_TOPC:def 5;

          then

          reconsider FA9 = FA as Subset-Family of Tu by ZFMISC_1: 82;

          

           A21: (TM | A) is second-countable by A9;

          FA is finite-ind by A11, A17, TOPDIM_1: 12;

          then

           A22: FA9 is finite-ind & ( ind FA) = ( ind FA9) by TOPDIM_1: 30;

          

           A23: FA9 is Cover of Tu by A20, SETFAM_1:def 11;

          then

           A24: Tu is finite-ind by A8, A9, A18, A19, A22;

          then

           A25: ( ind Tu) = ( ind uFA) by A20, TOPDIM_1: 22;

          ( ind Tu) <= (n - 1) by A8, A9, A18, A19, A22, A23;

          then

           A26: (( ind uFA) + 1) <= ((n - 1) + 1) by A25, XREAL_1: 6;

          

           A27: uFA is finite-ind by A24, TOPDIM_1: 18;

          A is finite-ind & ( ind A) <= 0 by A11, A12, A14, TOPDIM_1: 11;

          then ( [#] TM) is finite-ind & ( ind ( [#] TM)) <= (( ind uFA) + 1) by A16, A21, A27, TOPDIM_1: 40;

          hence thesis by A26, XXREAL_0: 2;

        end;

      end;

      for n holds P[n] from NAT_1:sch 2( A4, A7);

      then P[i1];

      hence thesis by A1, A2, A3;

    end;

    

     Lm4: A is finite-ind & B is finite-ind & (TM | (A \/ B)) is second-countable implies (A \/ B) is finite-ind & ( ind (A \/ B)) <= ((( ind A) + ( ind B)) + 1)

    proof

      assume that

       A1: A is finite-ind & B is finite-ind and

       A2: (TM | (A \/ B)) is second-countable;

      set AB = (A \/ B);

      set Tab = (TM | AB);

      ( [#] Tab) = AB by PRE_TOPC:def 5;

      then

      reconsider a = A, b = B as Subset of Tab by XBOOLE_1: 7;

      

       A3: a is finite-ind by A1, TOPDIM_1: 21;

      

      then

       A4: ( ind (Tab | a)) = ( ind a) by TOPDIM_1: 17

      .= ( ind A) by A1, TOPDIM_1: 21;

      ( [#] (Tab | b)) c= ( [#] Tab) by PRE_TOPC:def 4;

      then

       A5: ( bool ( [#] (Tab | b))) c= ( bool ( [#] Tab)) by ZFMISC_1: 67;

      

       A6: b is finite-ind by A1, TOPDIM_1: 21;

      then

      consider Fb be finite Subset-Family of (Tab | b) such that

       A7: Fb is Cover of (Tab | b) and

       A8: Fb is finite-ind and

       A9: ( ind Fb) <= 0 and

       A10: ( card Fb) <= (( ind (Tab | b)) + 1) and for a9,b9 be Subset of (Tab | b) st a9 in Fb & b9 in Fb & a9 meets b9 holds a9 = b9 by A2, Th7;

      consider Fa be finite Subset-Family of (Tab | a) such that

       A11: Fa is Cover of (Tab | a) and

       A12: Fa is finite-ind and

       A13: ( ind Fa) <= 0 and

       A14: ( card Fa) <= (( ind (Tab | a)) + 1) and for a9,b9 be Subset of (Tab | a) st a9 in Fa & b9 in Fa & a9 meets b9 holds a9 = b9 by A2, A3, Th7;

      ( [#] (Tab | a)) c= ( [#] Tab) by PRE_TOPC:def 4;

      then ( bool ( [#] (Tab | a))) c= ( bool ( [#] Tab)) by ZFMISC_1: 67;

      then

      reconsider FA = Fa, FB = Fb as finite Subset-Family of Tab by A5, XBOOLE_1: 1;

      

       A15: FB is finite-ind by A8, TOPDIM_1: 29;

      ( ind (Tab | b)) = ( ind b) by A6, TOPDIM_1: 17

      .= ( ind B) by A1, TOPDIM_1: 21;

      then ( card (FA \/ FB)) <= (( card FA) + ( card FB)) & (( card FA) + ( card FB)) <= ((( ind A) + 1) + (( ind B) + 1)) by A10, A14, A4, CARD_2: 43, XREAL_1: 7;

      then

       A16: ( card (FA \/ FB)) <= (((( ind A) + 1) + ( ind B)) + 1) by XXREAL_0: 2;

      ( union (FA \/ FB)) = (( union Fa) \/ ( union Fb)) by ZFMISC_1: 78

      .= (( [#] (Tab | a)) \/ ( union Fb)) by A11, SETFAM_1: 45

      .= (( [#] (Tab | a)) \/ ( [#] (Tab | b))) by A7, SETFAM_1: 45

      .= (a \/ ( [#] (Tab | b))) by PRE_TOPC:def 5

      .= (a \/ b) by PRE_TOPC:def 5

      .= ( [#] Tab) by PRE_TOPC:def 5;

      then

       A17: (FA \/ FB) is Cover of Tab by SETFAM_1:def 11;

      

       A18: ( ind FB) = ( ind Fb) by A8, TOPDIM_1: 29;

      

       A19: FA is finite-ind by A12, TOPDIM_1: 29;

      ( ind FA) = ( ind Fa) by A12, TOPDIM_1: 29;

      then

       A20: ( ind (FA \/ FB)) <= 0 by A9, A13, A19, A15, A18, TOPDIM_1: 13;

      then Tab is finite-ind by A2, A15, A16, A19, A17, Th8;

      then

       A21: AB is finite-ind by TOPDIM_1: 18;

      ( ind Tab) <= ((( ind A) + 1) + ( ind B)) by A2, A15, A16, A19, A17, A20, Th8;

      hence thesis by A21, TOPDIM_1: 17;

    end;

    registration

      let TM be second-countable metrizable TopSpace;

      let A,B be finite-ind Subset of TM;

      cluster (A \/ B) -> finite-ind;

      coherence

      proof

        (TM | (A \/ B)) is second-countable;

        hence thesis by Lm4;

      end;

    end

    theorem :: TOPDIM_2:9

    A is finite-ind & B is finite-ind & (TM | (A \/ B)) is second-countable implies (A \/ B) is finite-ind & ( ind (A \/ B)) <= ((( ind A) + ( ind B)) + 1) by Lm4;

    theorem :: TOPDIM_2:10

    

     Th10: for T1,T2 be TopSpace, A1 be Subset of T1, A2 be Subset of T2 holds ( Fr [:A1, A2:]) = ( [:( Fr A1), ( Cl A2):] \/ [:( Cl A1), ( Fr A2):])

    proof

      let T1,T2 be TopSpace, A1 be Subset of T1, A2 be Subset of T2;

      

       A1: ( [:( Cl A1), ( Cl A2):] /\ [:( Cl (A1 ` )), ( [#] T2):]) = [:(( Cl A1) /\ ( Cl (A1 ` ))), (( Cl A2) /\ ( [#] T2)):] by ZFMISC_1: 100

      .= [:( Fr A1), ( Cl A2):] by XBOOLE_1: 28;

      

       A2: ( [:( Cl A1), ( Cl A2):] /\ [:( [#] T1), ( Cl (A2 ` )):]) = [:(( Cl A1) /\ ( [#] T1)), (( Cl A2) /\ ( Cl (A2 ` ))):] by ZFMISC_1: 100

      .= [:( Cl A1), ( Fr A2):] by XBOOLE_1: 28;

      ( Cl ( [#] T1)) = ( [#] T1) by TOPS_1: 2;

      then

       A3: ( Cl [:( [#] T1), (A2 ` ):]) = [:( [#] T1), ( Cl (A2 ` )):] by TOPALG_3: 14;

      ( Cl ( [#] T2)) = ( [#] T2) by TOPS_1: 2;

      then

       A4: ( Cl [:(A1 ` ), ( [#] T2):]) = [:( Cl (A1 ` )), ( [#] T2):] by TOPALG_3: 14;

      ( Cl ( [:A1, A2:] ` )) = ( Cl ( [:( [#] T1), ( [#] T2):] \ [:A1, A2:])) by BORSUK_1:def 2

      .= ( Cl ( [:(( [#] T1) \ A1), ( [#] T2):] \/ [:( [#] T1), (( [#] T2) \ A2):])) by ZFMISC_1: 103

      .= ( [:( Cl (A1 ` )), ( [#] T2):] \/ [:( [#] T1), ( Cl (A2 ` )):]) by A4, A3, PRE_TOPC: 20;

      

      hence ( Fr [:A1, A2:]) = ( [:( Cl A1), ( Cl A2):] /\ ( [:( Cl (A1 ` )), ( [#] T2):] \/ [:( [#] T1), ( Cl (A2 ` )):])) by TOPALG_3: 14

      .= ( [:( Fr A1), ( Cl A2):] \/ [:( Cl A1), ( Fr A2):]) by A1, A2, XBOOLE_1: 23;

    end;

    

     Lm5: TM1 is non empty or TM2 is non empty implies [:TM1, TM2:] is finite-ind & ( ind [:TM1, TM2:]) <= (( ind TM1) + ( ind TM2))

    proof

      defpred P[ Nat] means for TM1, TM2 st (TM1 is non empty or TM2 is non empty) & ((( ind TM1) + ( ind TM2)) + 2) <= $1 holds [:TM1, TM2:] is finite-ind & ( ind [:TM1, TM2:]) <= (( ind TM1) + ( ind TM2));

      reconsider i1 = (( ind TM1) + 1), i2 = (( ind TM2) + 1) as Nat by Lm1;

      

       A1: for n st P[n] holds P[(n + 1)]

      proof

        let n such that

         A2: P[n];

        let TM1, TM2;

        assume that

         A3: TM1 is non empty or TM2 is non empty and

         A4: ((( ind TM1) + ( ind TM2)) + 2) <= (n + 1);

        set T12 = [:TM1, TM2:];

        per cases ;

          suppose

           A5: TM1 is empty;

          then ( ind TM1) = ( - 1) by TOPDIM_1: 6;

          then ( 0 + ( - 1)) <= (( ind TM2) + ( ind TM1)) by A3, XREAL_1: 6;

          hence thesis by A5, TOPDIM_1: 6;

        end;

          suppose

           A6: TM2 is empty;

          then ( ind TM2) = ( - 1) by TOPDIM_1: 6;

          then ( 0 + ( - 1)) <= (( ind TM1) + ( ind TM2)) by A3, XREAL_1: 6;

          hence thesis by A6, TOPDIM_1: 6;

        end;

          suppose

           A7: TM1 is non empty & TM2 is non empty;

          then

          reconsider i1 = ( ind TM1), i2 = ( ind TM2) as Nat by TARSKI: 1;

          

           A8: for p be Point of T12, U be open Subset of T12 st p in U holds ex W be open Subset of T12 st p in W & W c= U & ( Fr W) is finite-ind & ( ind ( Fr W)) <= ((i1 + i2) - 1)

          proof

            let p be Point of T12, U be open Subset of T12;

            consider F be Subset-Family of T12 such that

             A9: U = ( union F) and

             A10: for e be set st e in F holds ex X1 be Subset of TM1, X2 be Subset of TM2 st e = [:X1, X2:] & X1 is open & X2 is open by BORSUK_1: 5;

            assume p in U;

            then

            consider U12 be set such that

             A11: p in U12 and

             A12: U12 in F by A9, TARSKI:def 4;

            

             A13: U12 c= U by A9, A12, ZFMISC_1: 74;

            consider U1 be Subset of TM1, U2 be Subset of TM2 such that

             A14: U12 = [:U1, U2:] and

             A15: U1 is open and

             A16: U2 is open by A10, A12;

            consider p1,p2 be object such that

             A17: p1 in U1 and

             A18: p2 in U2 and

             A19: p = [p1, p2] by A11, A14, ZFMISC_1:def 2;

            reconsider p1 as Point of TM1 by A17;

            consider W1 be open Subset of TM1 such that

             A20: p1 in W1 and

             A21: W1 c= U1 and ( Fr W1) is finite-ind and

             A22: ( ind ( Fr W1)) <= (i1 - 1) by A15, A17, TOPDIM_1: 16;

            set ClW1 = ( Cl W1);

            

             A23: ( ind (TM1 | ClW1)) = ( ind ( Cl W1)) & ( ind ( Cl W1)) <= i1 by TOPDIM_1: 17, TOPDIM_1: 19;

            reconsider p2 as Point of TM2 by A18;

            consider W2 be open Subset of TM2 such that

             A24: p2 in W2 and

             A25: W2 c= U2 and ( Fr W2) is finite-ind and

             A26: ( ind ( Fr W2)) <= (i2 - 1) by A16, A18, TOPDIM_1: 16;

            reconsider W12 = [:W1, W2:] as open Subset of T12 by BORSUK_1: 6;

            take W12;

            W12 c= U12 by A14, A25, A21, ZFMISC_1: 96;

            hence p in W12 & W12 c= U by A13, A19, A24, A20, ZFMISC_1: 87;

            (((i1 + i2) + 1) + 1) <= (n + 1) by A4;

            then

             A27: ((i1 + i2) + 1) <= n by XREAL_1: 6;

            set FrW1 = ( Fr W1);

            

             A28: ( ind (TM1 | FrW1)) = ( ind ( Fr W1)) by TOPDIM_1: 17;

            set ClW2 = ( Cl W2);

            reconsider F1C2 = [:( Fr W1), ( Cl W2):] as Subset of T12;

            

             A29: [:(TM1 | FrW1), (TM2 | ClW2):] = (T12 | F1C2) by BORSUK_3: 22;

            ( ind (TM2 | ClW2)) = ( ind ( Cl W2)) & ( ind ( Cl W2)) <= i2 by TOPDIM_1: 17, TOPDIM_1: 19;

            then

             A30: (( ind (TM1 | FrW1)) + ( ind (TM2 | ClW2))) <= ((i1 - 1) + i2) by A22, A28, XREAL_1: 7;

            then ((( ind (TM1 | FrW1)) + ( ind (TM2 | ClW2))) + 2) <= (((i1 + i2) - 1) + 2) by XREAL_1: 6;

            then

             A31: W2 c= ( Cl W2) & ((( ind (TM1 | FrW1)) + ( ind (TM2 | ClW2))) + 2) <= n by A27, PRE_TOPC: 18, XXREAL_0: 2;

            then [:(TM1 | FrW1), (TM2 | ClW2):] is finite-ind by A2, A7, A24;

            then

             A32: F1C2 is finite-ind by A29, TOPDIM_1: 18;

            set FrW2 = ( Fr W2);

            reconsider C1F2 = [:( Cl W1), ( Fr W2):] as Subset of T12;

            

             A33: [:(TM1 | ClW1), (TM2 | FrW2):] = (T12 | C1F2) by BORSUK_3: 22;

            ( ind (TM2 | FrW2)) = ( ind ( Fr W2)) by TOPDIM_1: 17;

            then

             A34: (( ind (TM1 | ClW1)) + ( ind (TM2 | FrW2))) <= (i1 + (i2 - 1)) by A26, A23, XREAL_1: 7;

            then ((( ind (TM1 | ClW1)) + ( ind (TM2 | FrW2))) + 2) <= ((i1 + (i2 - 1)) + 2) by XREAL_1: 6;

            then

             A35: ((( ind (TM1 | ClW1)) + ( ind (TM2 | FrW2))) + 2) <= n by A27, XXREAL_0: 2;

            W1 c= ( Cl W1) & ( [#] (TM1 | ClW1)) = ClW1 by PRE_TOPC: 18, PRE_TOPC:def 5;

            then

             A36: (TM1 | ClW1) is non empty by A20;

            then [:(TM1 | ClW1), (TM2 | FrW2):] is finite-ind by A2, A35;

            then

             A37: C1F2 is finite-ind by A33, TOPDIM_1: 18;

            ( ind [:(TM1 | ClW1), (TM2 | FrW2):]) <= (( ind (TM1 | ClW1)) + ( ind (TM2 | FrW2))) by A2, A35, A36;

            then ( ind [:(TM1 | ClW1), (TM2 | FrW2):]) <= ((i1 + i2) - 1) by A34, XXREAL_0: 2;

            then

             A38: ( ind C1F2) <= ((i1 + i2) - 1) by A33, A37, TOPDIM_1: 17;

            

             A39: F1C2 is closed & (T12 | (C1F2 \/ F1C2)) is second-countable by TOPALG_3: 15;

            ( ind [:(TM1 | FrW1), (TM2 | ClW2):]) <= (( ind (TM1 | FrW1)) + ( ind (TM2 | ClW2))) by A2, A7, A24, A31;

            then ( ind [:(TM1 | FrW1), (TM2 | ClW2):]) <= ((i1 - 1) + i2) by A30, XXREAL_0: 2;

            then ( ind F1C2) <= ((i1 + i2) - 1) by A29, A32, TOPDIM_1: 17;

            then (C1F2 \/ F1C2) is finite-ind & ( ind (C1F2 \/ F1C2)) <= ((i1 + i2) - 1) by A39, A32, A37, A38, Th5;

            hence thesis by Th10;

          end;

          then T12 is finite-ind by TOPDIM_1: 15;

          hence thesis by A8, TOPDIM_1: 16;

        end;

      end;

      

       A40: P[ 0 ]

      proof

        let TM1, TM2;

        assume that

         A41: TM1 is non empty or TM2 is non empty and

         A42: ((( ind TM1) + ( ind TM2)) + 2) <= 0 ;

        reconsider i1 = (( ind TM1) + 1), i2 = (( ind TM2) + 1) as Nat by Lm1;

        (i1 + i2) <= 0 by A42;

        hence thesis by A41;

      end;

      

       A43: for n holds P[n] from NAT_1:sch 2( A40, A1);

      ((( ind TM1) + ( ind TM2)) + 2) = (i1 + i2);

      hence thesis by A43;

    end;

    registration

      let TM1, TM2;

      cluster [:TM1, TM2:] -> finite-ind;

      coherence

      proof

        per cases ;

          suppose TM1 is empty & TM2 is empty;

          hence thesis;

        end;

          suppose TM1 is non empty or TM2 is non empty;

          hence thesis by Lm5;

        end;

      end;

    end

    theorem :: TOPDIM_2:11

    

     Th11: for A, B st A is closed & B is closed & A misses B holds for H st ( ind H) <= n & (TM | H) is second-countable finite-ind holds ex L st L separates (A,B) & ( ind (L /\ H)) <= (n - 1)

    proof

      let A, B such that

       A1: A is closed & B is closed and

       A2: A misses B;

      let H such that

       A3: ( ind H) <= n and

       A4: (TM | H) is second-countable finite-ind;

      H is finite-ind by A4, TOPDIM_1: 18;

      then ( ind H) = ( ind (TM | H)) by TOPDIM_1: 17;

      then

      consider a,b be Subset of (TM | H) such that

       A5: ( [#] (TM | H)) = (a \/ b) and a misses b and

       A6: ( ind a) <= (n - 1) and

       A7: ( ind b) <= 0 by A3, A4, Lm3;

      ( [#] (TM | H)) c= ( [#] TM) by PRE_TOPC:def 4;

      then

      reconsider aa = a, bb = b as Subset of TM by XBOOLE_1: 1;

      

       A8: bb is finite-ind by A4, TOPDIM_1: 22;

      

       A9: H = (aa \/ bb) by A5, PRE_TOPC:def 5;

      then

       A10: (bb /\ H) = bb by XBOOLE_1: 7, XBOOLE_1: 28;

      ( ind b) = ( ind bb) & ((TM | H) | b) = (TM | bb) by A4, METRIZTS: 9, TOPDIM_1: 22;

      then

      consider L be Subset of TM such that

       A11: L separates (A,B) and

       A12: L misses bb by A1, A2, A4, A7, A8, TOPDIM_1: 37;

      take L;

      (L /\ H) misses bb & (L /\ H) c= H by A10, A12, XBOOLE_1: 17, XBOOLE_1: 76;

      then aa is finite-ind & (L /\ H) c= aa by A4, A9, TOPDIM_1: 22, XBOOLE_1: 73;

      then ( ind a) = ( ind aa) & ( ind (L /\ H)) <= ( ind aa) by TOPDIM_1: 19, TOPDIM_1: 21;

      hence thesis by A6, A11, XXREAL_0: 2;

    end;

    theorem :: TOPDIM_2:12

    for TM st TM is finite-ind second-countable & ( ind TM) <= n holds for A, B st A is closed & B is closed & A misses B holds ex L st L separates (A,B) & ( ind L) <= (n - 1)

    proof

      let TM such that

       A1: TM is finite-ind second-countable and

       A2: ( ind TM) <= n;

      

       A3: (TM | ( [#] TM)) is second-countable by A1;

      let A, B such that

       A4: A is closed & B is closed and

       A5: A misses B;

      consider L be Subset of TM such that

       A6: L separates (A,B) & ( ind (L /\ ( [#] TM))) <= (n - 1) by A4, A1, A2, A3, A5, Th11;

      take L;

      thus thesis by A6, XBOOLE_1: 28;

    end;

    theorem :: TOPDIM_2:13

    

     Th13: for H st (TM | H) is second-countable holds H is finite-ind & ( ind H) <= n iff for p, U st p in U holds ex W st p in W & W c= U & (H /\ ( Fr W)) is finite-ind & ( ind (H /\ ( Fr W))) <= (n - 1)

    proof

      let M be Subset of TM such that

       A1: (TM | M) is second-countable;

      hereby

        assume that

         A2: M is finite-ind and

         A3: ( ind M) <= n;

        let p be Point of TM, U be open Subset of TM such that

         A4: p in U;

        reconsider P = {p} as Subset of TM by A4, ZFMISC_1: 31;

        TM is non empty & not p in (U ` ) by A4, XBOOLE_0:def 5;

        then

        consider L be Subset of TM such that

         A5: L separates (P,(U ` )) and

         A6: ( ind (L /\ M)) <= (n - 1) by A1, A2, A3, Th11, ZFMISC_1: 50;

        consider W,W1 be open Subset of TM such that

         A7: P c= W and

         A8: (U ` ) c= W1 and

         A9: W misses W1 and

         A10: L = ((W \/ W1) ` ) by A5, METRIZTS:def 3;

        take W;

        W c= (W1 ` ) & (W1 ` ) c= ((U ` ) ` ) by A8, A9, SUBSET_1: 12, SUBSET_1: 23;

        hence p in W & W c= U by A7, ZFMISC_1: 31;

        ( Cl W) misses W1 by A9, TSEP_1: 36;

        then (( Cl W) \ W1) = ( Cl W) by XBOOLE_1: 83;

        

        then ( Fr W) = ((( Cl W) \ W1) \ W) by TOPS_1: 42

        .= (( Cl W) \ (W \/ W1)) by XBOOLE_1: 41

        .= (( Cl W) /\ L) by A10, SUBSET_1: 13;

        then ( Fr W) c= L by XBOOLE_1: 17;

        then

         A11: (M /\ ( Fr W)) c= (M /\ L) by XBOOLE_1: 27;

        (M /\ L) c= M by XBOOLE_1: 17;

        then

         A12: (M /\ L) is finite-ind by A2, TOPDIM_1: 19;

        then ( ind (M /\ ( Fr W))) <= ( ind (M /\ L)) by A11, TOPDIM_1: 19;

        hence (M /\ ( Fr W)) is finite-ind & ( ind (M /\ ( Fr W))) <= (n - 1) by A6, A11, A12, TOPDIM_1: 19, XXREAL_0: 2;

      end;

      set Tm = (TM | M);

      assume

       A13: for p be Point of TM, U be open Subset of TM st p in U holds ex W be open Subset of TM st p in W & W c= U & (M /\ ( Fr W)) is finite-ind & ( ind (M /\ ( Fr W))) <= (n - 1);

      

       A14: for p be Point of Tm, U be open Subset of Tm st p in U holds ex W be open Subset of Tm st p in W & W c= U & ( Fr W) is finite-ind & ( ind ( Fr W)) <= (n - 1)

      proof

        

         A15: ( [#] Tm) = M by PRE_TOPC:def 5;

        let p be Point of Tm, U be open Subset of Tm such that

         A16: p in U;

        p in M by A15, A16;

        then

        reconsider p9 = p as Point of TM;

        consider U9 be Subset of TM such that

         A17: U9 is open and

         A18: U = (U9 /\ the carrier of Tm) by TSP_1:def 1;

        p9 in U9 by A16, A18, XBOOLE_0:def 4;

        then

        consider W9 be open Subset of TM such that

         A19: p9 in W9 & W9 c= U9 and

         A20: (M /\ ( Fr W9)) is finite-ind and

         A21: ( ind (M /\ ( Fr W9))) <= (n - 1) by A13, A17;

        reconsider W = (W9 /\ the carrier of Tm) as Subset of Tm by XBOOLE_1: 17;

        reconsider W as open Subset of Tm by TSP_1:def 1;

        take W;

        thus p in W & W c= U by A16, A18, A19, XBOOLE_0:def 4, XBOOLE_1: 26;

        reconsider FrW = ( Fr W) as Subset of TM by A15, XBOOLE_1: 1;

        

         A22: FrW c= (( Fr W9) /\ M) by A15, TOPDIM_1: 1;

        then

         A23: FrW is finite-ind by A20, TOPDIM_1: 19;

        ( ind FrW) <= ( ind (( Fr W9) /\ M)) by A20, A22, TOPDIM_1: 19;

        then ( ind ( Fr W)) <= ( ind (( Fr W9) /\ M)) by A23, TOPDIM_1: 21;

        hence thesis by A21, A23, TOPDIM_1: 21, XXREAL_0: 2;

      end;

      then

       A24: Tm is finite-ind by TOPDIM_1: 15;

      then

       A25: M is finite-ind by TOPDIM_1: 18;

      ( ind Tm) <= n by A14, A24, TOPDIM_1: 16;

      hence thesis by A25, TOPDIM_1: 17;

    end;

    theorem :: TOPDIM_2:14

    for H st (TM | H) is second-countable holds H is finite-ind & ( ind H) <= n iff ex Bas be Basis of TM st for A st A in Bas holds (H /\ ( Fr A)) is finite-ind & ( ind (H /\ ( Fr A))) <= (n - 1)

    proof

      set cTM = ( [#] TM);

      set TOP = the topology of TM;

      let M be Subset of TM such that

       A1: (TM | M) is second-countable;

      hereby

        defpred P[ object, object] means for p be Point of TM, A be Subset of TM st $1 = [p, A] holds $2 in TOP & ( not p in A implies $2 = ( {} TM)) & (p in A implies ex W be open Subset of TM st W = $2 & p in W & W c= A & (M /\ ( Fr W)) is finite-ind & ( ind (M /\ ( Fr W))) <= (n - 1));

        assume

         A2: M is finite-ind & ( ind M) <= n;

        

         A3: for x be object st x in [:cTM, TOP:] holds ex y be object st P[x, y]

        proof

          let x be object such that

           A4: x in [:cTM, TOP:];

          consider p9,A9 be object such that

           A5: p9 in cTM and

           A6: A9 in TOP and

           A7: x = [p9, A9] by A4, ZFMISC_1:def 2;

          reconsider A9 as open Subset of TM by A6, PRE_TOPC:def 2;

          reconsider p9 as Point of TM by A5;

          per cases ;

            suppose

             A8: not p9 in A9;

            take ( {} TM);

            let p be Point of TM, A be Subset of TM such that

             A9: x = [p, A];

            p = p9 by A7, A9, XTUPLE_0: 1;

            hence thesis by A7, A8, A9, PRE_TOPC:def 2, XTUPLE_0: 1;

          end;

            suppose p9 in A9;

            then

            consider W be open Subset of TM such that

             A10: p9 in W & W c= A9 & (M /\ ( Fr W)) is finite-ind & ( ind (M /\ ( Fr W))) <= (n - 1) by A1, A2, Th13;

            take W;

            let p be Point of TM, A be Subset of TM such that

             A11: x = [p, A];

            p = p9 & A = A9 by A7, A11, XTUPLE_0: 1;

            hence thesis by A10, PRE_TOPC:def 2;

          end;

        end;

        consider f be Function such that

         A12: ( dom f) = [:cTM, TOP:] and

         A13: for x be object st x in [:cTM, TOP:] holds P[x, (f . x)] from CLASSES1:sch 1( A3);

        

         A14: ( rng f) c= TOP

        proof

          let y be object;

          assume y in ( rng f);

          then

          consider x be object such that

           A15: x in ( dom f) and

           A16: (f . x) = y by FUNCT_1:def 3;

          ex p,A be object st p in cTM & A in TOP & x = [p, A] by A12, A15, ZFMISC_1:def 2;

          hence thesis by A12, A13, A15, A16;

        end;

        then

        reconsider RNG = ( rng f) as Subset-Family of TM by XBOOLE_1: 1;

        now

          let A be Subset of TM such that

           A17: A is open;

          

           A18: A in TOP by A17, PRE_TOPC:def 2;

          let p be Point of TM such that

           A19: p in A;

          

           A20: [p, A] in [:cTM, TOP:] by A18, A19, ZFMISC_1: 87;

          then

          consider W be open Subset of TM such that

           A21: W = (f . [p, A]) & p in W & W c= A and (M /\ ( Fr W)) is finite-ind and ( ind (M /\ ( Fr W))) <= (n - 1) by A13, A19;

          reconsider W as Subset of TM;

          take W;

          thus W in RNG & p in W & W c= A by A12, A20, A21, FUNCT_1:def 3;

        end;

        then

        reconsider RNG as Basis of TM by A14, YELLOW_9: 32;

        take RNG;

        let B be Subset of TM;

        assume B in RNG;

        then

        consider x be object such that

         A22: x in ( dom f) and

         A23: (f . x) = B by FUNCT_1:def 3;

        consider p,A be object such that

         A24: p in cTM and

         A25: A in TOP and

         A26: x = [p, A] by A12, A22, ZFMISC_1:def 2;

        reconsider A as open Subset of TM by A25, PRE_TOPC:def 2;

        per cases ;

          suppose p in A;

          then ex W be open Subset of TM st W = (f . [p, A]) & p in W & W c= A & (M /\ ( Fr W)) is finite-ind & ( ind (M /\ ( Fr W))) <= (n - 1) by A12, A13, A22, A26;

          hence (M /\ ( Fr B)) is finite-ind & ( ind (M /\ ( Fr B))) <= (n - 1) by A23, A26;

        end;

          suppose not p in A;

          then B = ( {} TM) by A12, A13, A22, A23, A24, A26;

          then

           A27: ( Fr B) = {} by TOPGEN_1: 14;

          ( 0 - 1) <= (n - 1) by XREAL_1: 9;

          hence (M /\ ( Fr B)) is finite-ind & ( ind (M /\ ( Fr B))) <= (n - 1) by A27, TOPDIM_1: 6;

        end;

      end;

      given B be Basis of TM such that

       A28: for A be Subset of TM st A in B holds (M /\ ( Fr A)) is finite-ind & ( ind (M /\ ( Fr A))) <= (n - 1);

      for p be Point of TM, U be open Subset of TM st p in U holds ex W be open Subset of TM st p in W & W c= U & (M /\ ( Fr W)) is finite-ind & ( ind (M /\ ( Fr W))) <= (n - 1)

      proof

        let p be Point of TM, U be open Subset of TM such that

         A29: p in U;

        consider a be Subset of TM such that

         A30: a in B and

         A31: p in a & a c= U by A29, YELLOW_9: 31;

        B c= TOP by TOPS_2: 64;

        then

        reconsider a as open Subset of TM by A30, PRE_TOPC:def 2;

        take a;

        thus thesis by A28, A30, A31;

      end;

      hence thesis by A1, Th13;

    end;

    theorem :: TOPDIM_2:15

    TM1 is non empty or TM2 is non empty implies ( ind [:TM1, TM2:]) <= (( ind TM1) + ( ind TM2)) by Lm5;

    theorem :: TOPDIM_2:16

    ( ind TM2) = 0 implies ( ind [:TM1, TM2:]) = ( ind TM1)

    proof

      assume

       A1: ( ind TM2) = 0 ;

      then

       A2: TM2 is non empty by TOPDIM_1: 6;

      then

       A3: ( ind [:TM1, TM2:]) <= (( ind TM1) + 0 ) by A1, Lm5;

      set x = the Point of TM2;

      reconsider X = {x} as Subset of TM2 by A2, ZFMISC_1: 31;

      per cases ;

        suppose

         A4: TM1 is empty;

        then ( ind TM1) = ( - 1) by TOPDIM_1: 6;

        hence thesis by A4, TOPDIM_1: 6;

      end;

        suppose TM1 is non empty;

        then ( ind [:(TM2 | X), TM1:]) = ( ind TM1) by A2, BORSUK_3: 13, TOPDIM_1: 25;

        then

         A5: ( ind [:TM1, (TM2 | X):]) = ( ind TM1) by TOPDIM_1: 28;

        

         A6: [:TM1, (TM2 | X):] is SubSpace of [:TM1, TM2:] by BORSUK_3: 15;

        then ( [#] [:TM1, (TM2 | X):]) c= ( [#] [:TM1, TM2:]) by PRE_TOPC:def 4;

        then

        reconsider cT12 = ( [#] [:TM1, (TM2 | X):]) as Subset of [:TM1, TM2:];

         [:TM1, (TM2 | X):] = ( [:TM1, TM2:] | cT12) by A6, PRE_TOPC:def 5;

        then ( ind cT12) = ( ind TM1) by A5, TOPDIM_1: 17;

        then ( ind TM1) <= ( ind [:TM1, TM2:]) by TOPDIM_1: 19;

        hence thesis by A3, XXREAL_0: 1;

      end;

    end;

    begin

    reserve u for Point of ( Euclid 1),

U for Point of ( TOP-REAL 1),

r,u1 for Real,

s for Real;

    theorem :: TOPDIM_2:17

    

     Th17: <*u1*> = u implies ( cl_Ball (u,r)) = { <*s*> : (u1 - r) <= s & s <= (u1 + r) }

    proof

      assume that

       A1: <*u1*> = u;

      set E1 = { q where q be Element of ( Euclid 1) : ( dist (u,q)) <= r };

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

      set R1 = { <*s*> where s be Real : (u1 - r) <= s & s <= (u1 + r) };

      

       A2: E1 c= R1

      proof

        let x be object;

        assume x in E1;

        then

        consider q be Element of ( Euclid 1) such that

         A3: x = q and

         A4: ( dist (u,q)) <= r;

        q is Tuple of 1, REAL by FINSEQ_2: 131;

        then

        consider s1 be Element of REAL such that

         A5: q = <*s1*> by FINSEQ_2: 97;

        ( <*u1*> - <*s1*>) = <*(u1 - s1)*> by RVSUM_1: 29;

        then ( sqr ( <*u1*> - <*s1*>)) = <*((u1 - s1) ^2 )*> by RVSUM_1: 55;

        then ( Sum ( sqr ( <*u1*> - <*s1*>))) = ((u1 - s1) ^2 ) by RVSUM_1: 73;

        then

         A6: ( sqrt ( Sum ( sqr ( <*u1*> - <*s1*>)))) = |.(u1 - s1).| by COMPLEX1: 72;

        

         A7: |.( <*u1*> - <*s1*>).| <= r by A1, A4, A5, EUCLID:def 6;

        then (u1 - s1) <= r by A6, ABSVALUE: 5;

        then ((u1 - s1) + s1) <= (r + s1) by XREAL_1: 6;

        then

         A8: (u1 - r) <= ((r + s1) - r) by XREAL_1: 9;

        ( - r) <= (u1 - s1) by A6, A7, ABSVALUE: 5;

        then (( - r) + s1) <= ((u1 - s1) + s1) by XREAL_1: 6;

        then ((s1 - r) + r) <= (u1 + r) by XREAL_1: 6;

        hence thesis by A3, A5, A8;

      end;

      R1 c= E1

      proof

        reconsider eu1 = <*u1*> as Element of ( REAL 1) by FINSEQ_2: 98;

        let x be object;

        assume x in R1;

        then

        consider s be Real such that

         A9: x = <*s*> and

         A10: (u1 - r) <= s and

         A11: s <= (u1 + r);

        (s - r) <= ((u1 + r) - r) by A11, XREAL_1: 9;

        then

         A12: ((s + ( - r)) - s) <= (u1 - s) by XREAL_1: 9;

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

        reconsider es = <*s*> as Element of ( REAL 1) by FINSEQ_2: 98;

        reconsider q1 = <*s*> as Element of ( Euclid 1) by FINSEQ_2: 98;

        ( <*u1*> - <*s*>) = <*(u1 - s)*> by RVSUM_1: 29;

        then ( sqr ( <*u1*> - <*s*>)) = <*((u1 - s) ^2 )*> by RVSUM_1: 55;

        then

         A13: ( Sum ( sqr ( <*u1*> - <*s*>))) = ((u1 - s) ^2 ) by RVSUM_1: 73;

        ((u1 - r) + r) <= (s + r) by A10, XREAL_1: 6;

        then (u1 - s) <= ((s + r) - s) by XREAL_1: 9;

        then |.(u1 - s).| <= r by A12, ABSVALUE: 5;

        then |.( <*u1*> - <*s*>).| <= r by A13, COMPLEX1: 72;

        then (the distance of ( Euclid 1) . (u,q1)) = ( dist (u,q1)) & (( Pitag_dist 1) . (eu1,es)) <= r by EUCLID:def 6;

        hence thesis by A1, A9;

      end;

      then E1 = R1 by A2;

      hence thesis by METRIC_1: 18;

    end;

    

     Lm6: the TopStruct of ( TOP-REAL 1) = ( TopSpaceMetr ( Euclid 1)) by EUCLID:def 8;

    theorem :: TOPDIM_2:18

    

     Th18: <*u1*> = U & r > 0 implies ( Fr ( Ball (U,r))) = { <*(u1 - r)*>, <*(u1 + r)*>}

    proof

      assume that

       A1: <*u1*> = U and

       A2: r > 0 ;

      reconsider u = U as Point of ( Euclid 1) by Lm6;

      

       A3: ( Ball (u,r)) = { <*s*> : (u1 - r) < s & s < (u1 + r) } by A1, JORDAN2B: 27;

      ( Ball (U,r)) = ( Ball (u,r)) by TOPREAL9: 13;

      then ( Ball (U,r)) is open by KURATO_2: 1;

      

      then

       A4: ( Fr ( Ball (U,r))) = (( Cl ( Ball (U,r))) \ ( Ball (U,r))) by TOPS_1: 42

      .= (( cl_Ball (U,r)) \ ( Ball (U,r))) by A2, JORDAN: 23

      .= (( cl_Ball (u,r)) \ ( Ball (U,r))) by TOPREAL9: 14

      .= (( cl_Ball (u,r)) \ ( Ball (u,r))) by TOPREAL9: 13;

      

       A5: ( cl_Ball (u,r)) = { <*s*> : (u1 - r) <= s & s <= (u1 + r) } by A1, Th17;

      thus ( Fr ( Ball (U,r))) c= { <*(u1 - r)*>, <*(u1 + r)*>}

      proof

        let x be object such that

         A6: x in ( Fr ( Ball (U,r)));

        reconsider X = x as Point of ( Euclid 1) by Lm6, A6;

        x in ( cl_Ball (u,r)) by A4, A6, XBOOLE_0:def 5;

        then

        consider s be Real such that

         A7: x = <*s*> and

         A8: (u1 - r) <= s and

         A9: s <= (u1 + r) by A5;

        assume

         A10: not x in { <*(u1 - r)*>, <*(u1 + r)*>};

        then s <> (u1 + r) by A7, TARSKI:def 2;

        then

         A11: s < (u1 + r) by A9, XXREAL_0: 1;

        s <> (u1 - r) by A7, A10, TARSKI:def 2;

        then (u1 - r) < s by A8, XXREAL_0: 1;

        then X in ( Ball (u,r)) by A3, A7, A11;

        hence thesis by A4, A6, XBOOLE_0:def 5;

      end;

      let x be object;

      assume x in { <*(u1 - r)*>, <*(u1 + r)*>};

      then

       A12: x = <*(u1 - r)*> or x = <*(u1 + r)*> by TARSKI:def 2;

      assume

       A13: not x in ( Fr ( Ball (U,r)));

      (u1 + ( - r)) <= (u1 + r) by A2, XREAL_1: 6;

      then x in ( cl_Ball (u,r)) by A5, A12;

      then x in ( Ball (u,r)) by A4, A13, XBOOLE_0:def 5;

      then ex s be Real st x = <*s*> & (u1 - r) < s & s < (u1 + r) by A3;

      hence contradiction by A12, FINSEQ_1: 76;

    end;

    theorem :: TOPDIM_2:19

    

     Th19: for T be TopSpace, A be countable Subset of T st (T | A) is T_4 holds A is finite-ind & ( ind A) <= 0

    proof

      let T be TopSpace, A be countable Subset of T such that

       A1: (T | A) is T_4;

      per cases ;

        suppose A = ( {} T);

        hence thesis by TOPDIM_1: 6;

      end;

        suppose

         A2: A is non empty;

        then

        reconsider TT = T as non empty TopSpace;

        reconsider a = A as non empty Subset of TT by A2;

        set Ta = (TT | a);

        deffunc F( Point of Ta) = {$1};

        defpred P[ set] means not contradiction;

        defpred PP[ set] means $1 in A & P[$1];

        consider S be Subset-Family of Ta such that

         A3: S = { F(w) where w be Point of Ta : PP[w] } from LMOD_7:sch 5;

        for B be Subset of Ta st B in S holds B is finite-ind & ( ind B) <= 0

        proof

          let B be Subset of Ta;

          assume B in S;

          then

          consider w be Point of Ta such that

           A4: B = F(w) and PP[w] by A3;

          ( card F(w)) = 1 by CARD_1: 30;

          then ( ind F(w)) < (1 + 0 ) by TOPDIM_1: 8;

          hence thesis by A4, INT_1: 7;

        end;

        then

         A5: S is finite-ind & ( ind S) <= 0 by TOPDIM_1: 11;

        ( [#] Ta) c= ( union S)

        proof

          let x be object;

          assume

           A6: x in ( [#] Ta);

          then x in a by PRE_TOPC:def 5;

          then x in {x} & {x} in S by A3, A6, TARSKI:def 1;

          hence thesis by TARSKI:def 4;

        end;

        then

         A7: S is Cover of Ta by SETFAM_1:def 11;

        

         A8: S is closed

        proof

          let B be Subset of Ta;

          assume B in S;

          then ex w be Point of Ta st B = F(w) & PP[w] by A3;

          hence thesis by A1;

        end;

        

         A9: ( card A) c= omega by CARD_3:def 14;

        ( card { F(w) where w be Point of (TT | a) : PP[w] }) c= ( card A) from BORSUK_2:sch 1;

        then ( card S) c= omega by A3, A9;

        then

         A10: S is countable;

        ( [#] Ta) = A by PRE_TOPC:def 5;

        then

         A11: Ta is countable by ORDERS_4:def 2;

        then Ta is finite-ind by A1, A5, A7, A8, A10, TOPDIM_1: 36;

        then

         A12: A is finite-ind by TOPDIM_1: 18;

        ( ind Ta) <= 0 by A1, A5, A7, A8, A10, A11, TOPDIM_1: 36;

        hence thesis by A12, TOPDIM_1: 17;

      end;

    end;

    registration

      let TM be metrizable TopSpace;

      cluster countable -> finite-ind for Subset of TM;

      coherence

      proof

        let A be Subset of TM such that

         A1: A is countable;

        (TM | A) is T_4;

        hence thesis by A1, Th19;

      end;

    end

    

     Lm7: ( TOP-REAL 0 ) is finite-ind & ( ind ( TOP-REAL 0 )) = 0

    proof

      set T = ( TOP-REAL 0 );

       the TopStruct of T = ( TopSpaceMetr ( Euclid 0 )) by EUCLID:def 8;

      then

       A1: ( [#] T) = {( <*> REAL )} by FINSEQ_2: 94;

      ( card {( <*> REAL )}) = 1 by CARD_1: 30;

      then ( ind ( [#] T)) < 1 by A1, TOPDIM_1: 8;

      hence thesis by A1, NAT_1: 25;

    end;

    

     Lm8: ( TOP-REAL 1) is finite-ind & ( ind ( TOP-REAL 1)) = 1

    proof

      set T = ( TOP-REAL 1);

      

       A1: for p be Point of T, U be open Subset of T st p in U holds ex W be open Subset of T st p in W & W c= U & ( Fr W) is finite-ind & ( ind ( Fr W)) <= (1 - 1)

      proof

        let p be Point of T, U be open Subset of T such that

         A2: p in U;

        reconsider p9 = p as Point of ( Euclid 1) by Lm6;

        set M = ( Euclid 1);

        

         A3: the TopStruct of ( TopSpaceMetr M) = the TopStruct of ( TOP-REAL 1) by EUCLID:def 8;

        then

        reconsider V = U as Subset of ( TopSpaceMetr M);

        V is open by A3, PRE_TOPC: 30;

        then

        consider r be Real such that

         A4: r > 0 and

         A5: ( Ball (p9,r)) c= U by A2, TOPMETR: 15;

        reconsider B = ( Ball (p9,r)) as open Subset of T by KURATO_2: 1;

        take B;

        p9 is Tuple of 1, REAL by FINSEQ_2: 131;

        then

        consider p1 be Element of REAL such that

         A6: p9 = <*p1*> by FINSEQ_2: 97;

        

         A7: ( Ball (p,r)) = ( Ball (p9,r)) by TOPREAL9: 13;

        then

         A8: ( Fr B) = { <*(p1 - r)*>, <*(p1 + r)*>} by A4, A6, Th18;

        T is metrizable by A3, PCOMPS_1:def 8;

        then (T | ( Fr B)) is metrizable;

        hence thesis by A4, A5, A7, Th19, A8, JORDAN: 16;

      end;

      then

       A9: T is finite-ind by TOPDIM_1: 15;

      

       A10: ( ind T) >= 1

      proof

        reconsider jj = 1 as Element of REAL by XREAL_0:def 1;

        reconsider p = <*( In ( 0 , REAL ))*>, q = <*jj*> as Point of ( Euclid 1) by FINSEQ_2: 98;

         the TopStruct of T = ( TopSpaceMetr ( Euclid 1)) by EUCLID:def 8;

        then

        reconsider p9 = p as Point of T;

        

         A11: ( Ball (p,1)) = ( Ball (p9,1)) by TOPREAL9: 13;

        then

        reconsider B = ( Ball (p9,1)) as open Subset of T by KURATO_2: 1;

        assume ( ind T) < 1;

        then ( ind T) < (1 + 0 );

        then

         A12: ( ind T) <= 0 by INT_1: 7;

        p in B by JORDAN: 16;

        then

        consider W be open Subset of T such that

         A13: p in W and

         A14: W c= B and

         A15: ( Fr W) is finite-ind & ( ind ( Fr W)) <= ( 0 - 1) by A9, A12, TOPDIM_1: 16;

        ( Fr W) = ( {} T) by A15;

        then

         A16: W is closed by TOPGEN_1: 14;

        

         A17: (W \/ (W ` )) = ( [#] T) by PRE_TOPC: 2;

        W misses (W ` ) by SUBSET_1: 24;

        then ( [#] T) is convex & (W,(W ` )) are_separated by A16, CONNSP_1: 2;

        then

         A18: (W ` ) = ( {} T) by A13, A17, CONNSP_1: 15;

        

         A19: B = { <*s*> where s be Real : ( 0 - 1) < s & s < ( 0 + 1) } by A11, JORDAN2B: 27;

        

         A20: the TopStruct of T = ( TopSpaceMetr ( Euclid 1)) by EUCLID:def 8;

         not q in B

        proof

          assume q in B;

          then ex s be Real st q = <*s*> & ( 0 - 1) < s & s < ( 0 + 1) by A19;

          hence contradiction by FINSEQ_1: 76;

        end;

        then not q in W by A14;

        hence contradiction by A20, A18, XBOOLE_0:def 5;

      end;

      ( ind T) <= 1 by A1, A9, TOPDIM_1: 16;

      hence thesis by A1, A10, TOPDIM_1: 15, XXREAL_0: 1;

    end;

    

     Lm9: ( TOP-REAL n) is finite-ind & ( ind ( TOP-REAL n)) <= n

    proof

      defpred P[ Nat] means ( TOP-REAL $1) is finite-ind & ( ind ( TOP-REAL $1)) <= $1;

      

       A1: for n st P[n] holds P[(n + 1)]

      proof

        let n;

        

         A2: the TopStruct of ( TOP-REAL n) = ( TopSpaceMetr ( Euclid n)) & the TopStruct of ( TOP-REAL (n + 1)) = ( TopSpaceMetr ( Euclid (n + 1))) & the TopStruct of ( TOP-REAL 1) = ( TopSpaceMetr ( Euclid 1)) by EUCLID:def 8;

        

         A3: n in NAT by ORDINAL1:def 12;

        then

         A4: ( [:( TopSpaceMetr ( Euclid n)), ( TopSpaceMetr ( Euclid 1)):],( TopSpaceMetr ( Euclid (n + 1)))) are_homeomorphic by TOPREAL7: 25;

        (( TOP-REAL 1),( TopSpaceMetr ( Euclid 1))) are_homeomorphic by A2, YELLOW14: 19;

        then

         A5: ( TopSpaceMetr ( Euclid 1)) is finite-ind & ( ind ( TopSpaceMetr ( Euclid 1))) = 1 by Lm8, TOPDIM_1: 24, TOPDIM_1: 25;

        assume

         A6: P[n];

        

         A7: (( TOP-REAL n),( TopSpaceMetr ( Euclid n))) are_homeomorphic by A2, YELLOW14: 19;

        

         A8: (( TOP-REAL (n + 1)),( TopSpaceMetr ( Euclid (n + 1)))) are_homeomorphic by A2, YELLOW14: 19;

        

         A9: ( TopSpaceMetr ( Euclid n)) is finite-ind & ( ind ( TopSpaceMetr ( Euclid n))) = ( ind ( TOP-REAL n)) by A6, A7, TOPDIM_1: 24, TOPDIM_1: 25;

        then

         A10: ( ind [:( TopSpaceMetr ( Euclid n)), ( TopSpaceMetr ( Euclid 1)):]) <= (( ind ( TopSpaceMetr ( Euclid n))) + 1) by Lm5, A2, A5;

        (( ind ( TopSpaceMetr ( Euclid n))) + 1) <= (n + 1) by A6, A9, XREAL_1: 6;

        then ( ind [:( TopSpaceMetr ( Euclid n)), ( TopSpaceMetr ( Euclid 1)):]) <= (n + 1) by A10, XXREAL_0: 2;

        then

         A11: ( ind ( TopSpaceMetr ( Euclid (n + 1)))) <= (n + 1) by A3, A9, A5, A2, TOPDIM_1: 25, TOPREAL7: 25;

        ( TopSpaceMetr ( Euclid (n + 1))) is finite-ind by A9, A5, A2, A4, TOPDIM_1: 24;

        then ( TOP-REAL (n + 1)) is finite-ind by A8, TOPDIM_1: 24;

        hence thesis by A11, A2, TOPDIM_1: 25, YELLOW14: 19;

      end;

      

       A12: P[ 0 ] by Lm7;

      for n holds P[n] from NAT_1:sch 2( A12, A1);

      hence thesis;

    end;

    registration

      let n be Nat;

      cluster ( TOP-REAL n) -> finite-ind;

      coherence by Lm9;

    end

    theorem :: TOPDIM_2:20

    n <= 1 implies ( ind ( TOP-REAL n)) = n

    proof

      assume n <= 1;

      then n < 1 or n = 1 by XXREAL_0: 1;

      then n = 0 or n = 1 by NAT_1: 14;

      hence thesis by Lm7, Lm8;

    end;

    theorem :: TOPDIM_2:21

    ( ind ( TOP-REAL n)) <= n by Lm9;

    

     Lm10: for A be finite-ind Subset of TM st (TM | A) is second-countable & ( ind (TM | A)) <= 0 holds for U1,U2 be open Subset of TM st A c= (U1 \/ U2) holds ex V1,V2 be open Subset of TM st V1 c= U1 & V2 c= U2 & V1 misses V2 & A c= (V1 \/ V2)

    proof

      let A be finite-ind Subset of TM such that

       A1: (TM | A) is second-countable & ( ind (TM | A)) <= 0 ;

      let U1,U2 be open Subset of TM such that

       A2: A c= (U1 \/ U2);

      set U12 = (U1 \/ U2);

      set TU = (TM | U12);

      

       A3: ( [#] TU) = U12 by PRE_TOPC:def 5;

      then

      reconsider u1 = U1, u2 = U2, a = A as Subset of TU by A2, XBOOLE_1: 7;

      

       A4: a is finite-ind by TOPDIM_1: 21;

      

       A5: (u1 ` ) misses (u2 ` )

      proof

        assume (u1 ` ) meets (u2 ` );

        then

        consider z be object such that

         A6: z in (u1 ` ) and

         A7: z in (u2 ` ) by XBOOLE_0: 3;

        ( not z in U1) & not z in U2 by A6, A7, XBOOLE_0:def 5;

        hence thesis by A3, A6, XBOOLE_0:def 3;

      end;

      (U2 /\ U12) = u2 by XBOOLE_1: 7, XBOOLE_1: 28;

      then

       A8: u2 is open by A3, TSP_1:def 1;

      (U1 /\ U12) = u1 by XBOOLE_1: 7, XBOOLE_1: 28;

      then

       A9: u1 is open by A3, TSP_1:def 1;

      

       A10: ( ind a) = ( ind A) by TOPDIM_1: 21;

      ( ind A) <= 0 & (TU | a) is second-countable by A1, METRIZTS: 9, TOPDIM_1: 17;

      then

      consider L be Subset of TU such that

       A11: L separates ((u1 ` ),(u2 ` )) and

       A12: ( ind (L /\ a)) <= ( 0 - 1) by A4, A5, A9, A8, A10, Th11;

      consider v1,v2 be open Subset of TU such that

       A13: (u1 ` ) c= v1 & (u2 ` ) c= v2 and

       A14: v1 misses v2 and

       A15: L = ((v1 \/ v2) ` ) by A11, METRIZTS:def 3;

      reconsider V1 = v1, V2 = v2 as Subset of TM by A3, XBOOLE_1: 1;

      reconsider V1, V2 as open Subset of TM by A3, TSEP_1: 9;

      take V2, V1;

      (u1 ` ) misses v2 & (u2 ` ) misses v1 by A13, A14, XBOOLE_1: 63;

      hence V2 c= U1 & V1 c= U2 & V2 misses V1 by A14, SUBSET_1: 24;

      (L /\ a) c= a by XBOOLE_1: 17;

      then

       A16: (L /\ a) is finite-ind by A4, TOPDIM_1: 19;

      then ( ind (L /\ a)) >= ( - 1) by TOPDIM_1: 5;

      then ( ind (L /\ a)) = ( - 1) by A12, XXREAL_0: 1;

      then (L /\ a) is empty by A16;

      then L misses a;

      hence thesis by A15, SUBSET_1: 24;

    end;

    theorem :: TOPDIM_2:22

    

     Th22: for A st (TM | A) is second-countable finite-ind & ( ind A) <= 0 holds for F st F is open & F is Cover of A holds ex g be Function of F, ( bool the carrier of TM) st ( rng g) is open & ( rng g) is Cover of A & (for a be set st a in F holds (g . a) c= a) & for a,b be set st a in F & b in F & a <> b holds (g . a) misses (g . b)

    proof

      defpred P[ Nat] means for A be Subset of TM st (TM | A) is second-countable & A is finite-ind & ( ind A) <= 0 holds for F be finite Subset-Family of TM st F is open & F is Cover of A & ( card F) <= $1 holds ex g be Function of F, ( bool the carrier of TM) st ( rng g) is open & ( rng g) is Cover of A & (for a be set st a in F holds (g . a) c= a) & for a,b be set st a in F & b in F & a <> b holds (g . a) misses (g . b);

      let A be Subset of TM such that

       A1: (TM | A) is second-countable finite-ind & ( ind A) <= 0 ;

      let F be finite Subset-Family of TM such that

       A2: F is open & F is Cover of A;

      

       A3: for n st P[n] holds P[(n + 1)]

      proof

        let n such that

         A4: P[n];

        let A be Subset of TM such that

         A5: (TM | A) is second-countable and

         A6: A is finite-ind and

         A7: ( ind A) <= 0 ;

        let F be finite Subset-Family of TM such that

         A8: F is open and

         A9: F is Cover of A and

         A10: ( card F) <= (n + 1);

        per cases by A10, NAT_1: 8;

          suppose ( card F) <= n;

          hence thesis by A4, A5, A6, A7, A8, A9;

        end;

          suppose

           A11: ( card F) = (n + 1);

          per cases ;

            suppose n = 0 ;

            then

            consider x be object such that

             A12: F = {x} by A11, CARD_2: 42;

            set g = (F --> x);

            ( dom g) = F & ( rng g) = F by A12, FUNCOP_1: 8, FUNCOP_1: 13;

            then

            reconsider g as Function of F, ( bool the carrier of TM) by FUNCT_2: 2;

            take g;

            thus ( rng g) is open & ( rng g) is Cover of A by A8, A9, A12, FUNCOP_1: 8;

            hereby

              let a be set;

              assume

               A13: a in F;

              then (g . a) = x by FUNCOP_1: 7;

              hence (g . a) c= a by A12, A13, TARSKI:def 1;

            end;

            let a,b be set such that

             A14: a in F and

             A15: b in F & a <> b;

            x = a by A12, A14, TARSKI:def 1;

            hence thesis by A12, A15, TARSKI:def 1;

          end;

            suppose n > 0 ;

            then

            reconsider n1 = (n - 1) as Element of NAT by NAT_1: 20;

            F is non empty by A11;

            then

            consider x be object such that

             A16: x in F;

            

             A17: ( card (F \ {x})) = (n1 + 1) by A11, A16, STIRL2_1: 55;

            then (F \ {x}) is non empty;

            then

            consider y be object such that

             A18: y in (F \ {x});

            y in F by A18, XBOOLE_0:def 5;

            then

            reconsider x, y as open Subset of TM by A8, A16;

            set X = {x}, xy = (x \/ y), Y = {y}, XY = {xy};

            

             A19: ((F \ X) \/ X) = F by A16, ZFMISC_1: 116;

            set Fxy = ((F \ X) \ Y);

            

             A20: ( card Fxy) = n1 by A17, A18, STIRL2_1: 55;

            set FXY = (Fxy \/ XY);

            ( card XY) = 1 by CARD_1: 30;

            then

             A21: ( card FXY) <= (n1 + 1) by A20, CARD_2: 43;

            (F \ X) is open by A8, TOPS_2: 15;

            then

             A22: Fxy is open by TOPS_2: 15;

            

             A23: (((F \ X) \ Y) \/ Y) = (F \ X) by A18, ZFMISC_1: 116;

            for A be Subset of TM st A in XY holds A is open by TARSKI:def 1;

            then

             A24: XY is open;

            per cases ;

              suppose

               A25: Fxy is Cover of A;

              ( card Fxy) <= (n1 + 1) by A20, NAT_1: 13;

              then

              consider g be Function of Fxy, ( bool the carrier of TM) such that

               A26: ( rng g) is open and

               A27: ( rng g) is Cover of A and

               A28: for a be set st a in Fxy holds (g . a) c= a and

               A29: for a,b be set st a in Fxy & b in Fxy & a <> b holds (g . a) misses (g . b) by A4, A5, A6, A7, A22, A25;

              

               A30: A c= ( union ( rng g)) by A27, SETFAM_1:def 11;

              set h = ((x,y) --> (( {} TM),( {} TM)));

              

               A31: ( dom h) = {x, y} by FUNCT_4: 62;

               not x in (F \ X) by ZFMISC_1: 56;

              then

               A32: not x in Fxy by ZFMISC_1: 56;

               not y in Fxy by ZFMISC_1: 56;

              then

               A33: Fxy misses {x, y} by A32, ZFMISC_1: 51;

              

               A34: x <> y by A18, ZFMISC_1: 56;

              then

               A35: ( rng h) = {( {} TM), ( {} TM)} by FUNCT_4: 64;

              

               A36: (Fxy \/ {x, y}) = (Fxy \/ (Y \/ X)) by ENUMSET1: 1

              .= ((Fxy \/ Y) \/ X) by XBOOLE_1: 4

              .= F by A18, A19, ZFMISC_1: 116;

              

               A37: ( dom g) = Fxy by FUNCT_2:def 1;

              then

               A38: ( rng (g +* h)) = (( rng g) \/ ( rng h)) by A31, A33, NECKLACE: 6;

              ( dom (g +* h)) = (Fxy \/ {x, y}) by A31, A37, FUNCT_4:def 1;

              then

              reconsider gh = (g +* h) as Function of F, ( bool the carrier of TM) by A36, A38, FUNCT_2: 2;

              take gh;

              (h . y) = ( {} TM) & y in {x, y} by FUNCT_4: 63, TARSKI:def 2;

              then

               A39: (gh . y) = ( {} TM) by A31, FUNCT_4: 13;

              for A be Subset of TM st A in {( {} TM), ( {} TM)} holds A is open by TARSKI:def 2;

              then {( {} TM), ( {} TM)} is open;

              hence ( rng gh) is open by A26, A35, A38, TOPS_2: 13;

              ( union ( rng gh)) = (( union ( rng g)) \/ ( union ( rng h))) by A38, ZFMISC_1: 78

              .= (( union ( rng g)) \/ ( union {( {} TM)})) by A35, ENUMSET1: 29

              .= (( union ( rng g)) \/ ( {} TM)) by ZFMISC_1: 25

              .= ( union ( rng g));

              hence ( rng gh) is Cover of A by A30, SETFAM_1:def 11;

              x in {x, y} & (h . x) = ( {} TM) by A34, FUNCT_4: 63, TARSKI:def 2;

              then

               A40: (gh . x) = ( {} TM) by A31, FUNCT_4: 13;

              hereby

                let a be set;

                assume

                 A41: a in F;

                per cases by A36, A41, XBOOLE_0:def 3;

                  suppose a in Fxy;

                  then ( not a in ( dom h)) & (g . a) c= a by A28, A33, XBOOLE_0: 3;

                  hence (gh . a) c= a by FUNCT_4: 11;

                end;

                  suppose a in {x, y};

                  then a = x or a = y by TARSKI:def 2;

                  hence (gh . a) c= a by A39, A40;

                end;

              end;

              let a,b be set such that

               A42: a in F & b in F and

               A43: a <> b;

              per cases by A36, A42, XBOOLE_0:def 3;

                suppose

                 A44: a in Fxy & b in Fxy;

                then not a in ( dom h) by A33, XBOOLE_0: 3;

                then

                 A45: (gh . a) = (g . a) by FUNCT_4: 11;

                ( not b in ( dom h)) & (g . a) misses (g . b) by A29, A33, A43, A44, XBOOLE_0: 3;

                hence thesis by A45, FUNCT_4: 11;

              end;

                suppose a in {x, y} or b in {x, y};

                then (gh . a) = ( {} TM) or (gh . b) = ( {} TM) by A39, A40, TARSKI:def 2;

                hence thesis;

              end;

            end;

              suppose

               A46: not Fxy is Cover of A;

              

               A47: (( union Fxy) \/ xy) = (( union Fxy) \/ ( union XY)) by ZFMISC_1: 25

              .= ( union FXY) by ZFMISC_1: 78;

              

               A48: FXY is open by A22, A24, TOPS_2: 13;

              

               A49: ( union F) = (( union (F \ X)) \/ ( union X)) by A19, ZFMISC_1: 78

              .= (( union (F \ X)) \/ x) by ZFMISC_1: 25

              .= ((( union Fxy) \/ ( union Y)) \/ x) by A23, ZFMISC_1: 78

              .= ((( union Fxy) \/ y) \/ x) by ZFMISC_1: 25

              .= (( union Fxy) \/ (y \/ x)) by XBOOLE_1: 4;

              A c= ( union F) by A9, SETFAM_1:def 11;

              then FXY is Cover of A by A47, A49, SETFAM_1:def 11;

              then

              consider g be Function of FXY, ( bool the carrier of TM) such that

               A50: ( rng g) is open and

               A51: ( rng g) is Cover of A and

               A52: for a be set st a in FXY holds (g . a) c= a and

               A53: for a,b be set st a in FXY & b in FXY & a <> b holds (g . a) misses (g . b) by A4, A5, A6, A7, A21, A48;

              

               A54: ( rng (g | Fxy)) is open by A50, RELAT_1: 70, TOPS_2: 11;

              xy in XY by TARSKI:def 1;

              then

               A55: xy in FXY by XBOOLE_0:def 3;

              then

               A56: (g . xy) c= xy by A52;

              

               A57: ( dom g) = FXY by FUNCT_2:def 1;

              

              then

               A58: ( dom (g | Fxy)) = (FXY /\ Fxy) by RELAT_1: 61

              .= Fxy by XBOOLE_1: 21;

              (g . xy) in ( rng g) by A55, A57, FUNCT_1:def 3;

              then

              reconsider gxy = (g . xy) as open Subset of TM by A50;

              set gxyA = (gxy /\ A);

              gxyA c= gxy by XBOOLE_1: 17;

              then

               A59: gxyA c= xy by A56;

              ( [#] (TM | A)) = A by PRE_TOPC:def 5;

              then

              reconsider GxyA = gxyA as Subset of (TM | A) by XBOOLE_1: 17;

              

               A60: ((TM | A) | GxyA) = (TM | gxyA) by METRIZTS: 9;

              (TM | A) is finite-ind by A6;

              then

               A61: gxyA is finite-ind by A60, TOPDIM_1: 18;

              then

               A62: ( ind gxyA) = ( ind (TM | gxyA)) by TOPDIM_1: 17;

              ( ind GxyA) <= ( ind (TM | A)) by A6, TOPDIM_1: 19;

              then ( ind GxyA) <= 0 by A6, A7, TOPDIM_1: 17;

              then ( ind gxyA) <= 0 by A61, TOPDIM_1: 21;

              then

              consider V1,V2 be open Subset of TM such that

               A63: V1 c= x & V2 c= y and

               A64: V1 misses V2 and

               A65: gxyA c= (V1 \/ V2) by A5, A59, A60, A61, A62, Lm10;

              reconsider gV1 = (gxy /\ V1), gV2 = (gxy /\ V2) as open Subset of TM;

              set h = ((x,y) --> (gV1,gV2));

              

               A66: ( dom h) = {x, y} by FUNCT_4: 62;

              then

               A67: ( dom ((g | Fxy) +* h)) = (Fxy \/ {x, y}) by A58, FUNCT_4:def 1;

               not x in (F \ X) by ZFMISC_1: 56;

              then

               A68: not x in Fxy by ZFMISC_1: 56;

              

               A69: x in {x, y} by TARSKI:def 2;

              

               A70: (Fxy \/ {x, y}) = (Fxy \/ (Y \/ X)) by ENUMSET1: 1

              .= ((Fxy \/ Y) \/ X) by XBOOLE_1: 4

              .= F by A18, A19, ZFMISC_1: 116;

              for A be Subset of TM st A in {gV1, gV2} holds A is open by TARSKI:def 2;

              then

               A71: {gV1, gV2} is open;

              

               A72: y in {x, y} by TARSKI:def 2;

               not y in Fxy by ZFMISC_1: 56;

              then

               A73: Fxy misses {x, y} by A68, ZFMISC_1: 51;

              then

               A74: ( rng ((g | Fxy) +* h)) = (( rng (g | Fxy)) \/ ( rng h)) by A58, A66, NECKLACE: 6;

              then

              reconsider gh = ((g | Fxy) +* h) as Function of F, ( bool the carrier of TM) by A67, A70, FUNCT_2: 2;

              

               A75: Fxy c= ( dom gh) by A67, XBOOLE_1: 7;

              take gh;

              

               A76: x <> y by A18, ZFMISC_1: 56;

              then ( rng h) = {gV1, gV2} by FUNCT_4: 64;

              hence ( rng gh) is open by A54, A71, A74, TOPS_2: 13;

              (h . x) = gV1 by A76, FUNCT_4: 63;

              then

               A77: (gh . x) = gV1 by A66, A69, FUNCT_4: 13;

              (h . y) = gV2 by FUNCT_4: 63;

              then

               A78: (gh . y) = gV2 by A66, A72, FUNCT_4: 13;

              

               A79: for a,b be set st a in Fxy & b in {x, y} & a <> b holds (gh . a) misses (gh . b)

              proof

                xy in XY by TARSKI:def 1;

                then

                 A80: xy in FXY by XBOOLE_0:def 3;

                let a,b be set such that

                 A81: a in Fxy and

                 A82: b in {x, y} and a <> b;

                ((g | Fxy) . a) = (g . a) & not a in ( dom h) by A58, A73, A81, FUNCT_1: 47, XBOOLE_0: 3;

                then

                 A83: (gh . a) = (g . a) by FUNCT_4: 11;

                

                 A84: a <> xy

                proof

                  assume a = xy;

                  then

                   A85: ( union F) = ( union Fxy) by A49, A81, XBOOLE_1: 12, ZFMISC_1: 74;

                   not A c= ( union Fxy) by A46, SETFAM_1:def 11;

                  hence thesis by A9, A85, SETFAM_1:def 11;

                end;

                assume (gh . a) meets (gh . b);

                then

                consider z be object such that

                 A86: z in (gh . a) and

                 A87: z in (gh . b) by XBOOLE_0: 3;

                z in gV1 or z in gV2 by A78, A77, A82, A87, TARSKI:def 2;

                then z in gxy by XBOOLE_0:def 4;

                then (g . xy) meets (g . a) by A83, A86, XBOOLE_0: 3;

                hence thesis by A53, A58, A80, A81, A84;

              end;

              

               A88: {x, y} c= ( dom gh) by A67, XBOOLE_1: 7;

              then

               A89: (gh . y) in ( rng gh) by A72, FUNCT_1:def 3;

              

               A90: (gh . x) in ( rng gh) by A69, A88, FUNCT_1:def 3;

              A c= ( union ( rng gh))

              proof

                let z be object such that

                 A91: z in A;

                A c= ( union ( rng g)) by A51, SETFAM_1:def 11;

                then

                consider G be set such that

                 A92: z in G and

                 A93: G in ( rng g) by A91, TARSKI:def 4;

                consider Gx be object such that

                 A94: Gx in FXY and

                 A95: (g . Gx) = G by A57, A93, FUNCT_1:def 3;

                per cases by A94, XBOOLE_0:def 3;

                  suppose

                   A96: Gx in Fxy;

                  then ((g | Fxy) . Gx) = G & not Gx in ( dom h) by A58, A73, A95, FUNCT_1: 47, XBOOLE_0: 3;

                  then

                   A97: (gh . Gx) = G by FUNCT_4: 11;

                  (gh . Gx) in ( rng gh) by A75, A96, FUNCT_1:def 3;

                  hence thesis by A92, A97, TARSKI:def 4;

                end;

                  suppose Gx in XY;

                  then

                   A98: z in gxy by A92, A95, TARSKI:def 1;

                  then z in gxyA by A91, XBOOLE_0:def 4;

                  then z in V1 or z in V2 by A65, XBOOLE_0:def 3;

                  then z in gV1 or z in gV2 by A98, XBOOLE_0:def 4;

                  hence thesis by A78, A77, A90, A89, TARSKI:def 4;

                end;

              end;

              hence ( rng gh) is Cover of A by SETFAM_1:def 11;

              

               A99: gV1 c= V1 & gV2 c= V2 by XBOOLE_1: 17;

              hereby

                let a be set;

                assume

                 A100: a in F;

                per cases by A70, A100, XBOOLE_0:def 3;

                  suppose

                   A101: a in Fxy;

                  then

                   A102: ((g | Fxy) . a) = (g . a) by A58, FUNCT_1: 47;

                  ( not a in ( dom h)) & (g . a) c= a by A52, A58, A73, A101, XBOOLE_0: 3;

                  hence (gh . a) c= a by A102, FUNCT_4: 11;

                end;

                  suppose a in {x, y};

                  then a = x or a = y by TARSKI:def 2;

                  hence (gh . a) c= a by A63, A78, A77, A99;

                end;

              end;

              let a,b be set such that

               A103: a in F & b in F and

               A104: a <> b;

              per cases by A70, A103, XBOOLE_0:def 3;

                suppose

                 A105: a in Fxy & b in Fxy;

                then ((g | Fxy) . a) = (g . a) & not a in ( dom h) by A58, A73, FUNCT_1: 47, XBOOLE_0: 3;

                then

                 A106: (gh . a) = (g . a) by FUNCT_4: 11;

                

                 A107: ((g | Fxy) . b) = (g . b) & not b in ( dom h) by A58, A73, A105, FUNCT_1: 47, XBOOLE_0: 3;

                (g . a) misses (g . b) by A53, A58, A104, A105;

                hence thesis by A106, A107, FUNCT_4: 11;

              end;

                suppose a in Fxy & b in {x, y} or a in {x, y} & b in Fxy;

                hence thesis by A79, A104;

              end;

                suppose

                 A108: a in {x, y} & b in {x, y};

                then a = x or a = y by TARSKI:def 2;

                then a = x & b = y or a = y & b = x by A104, A108, TARSKI:def 2;

                hence thesis by A64, A78, A77, A99, XBOOLE_1: 64;

              end;

            end;

          end;

        end;

      end;

      

       A109: P[ 0 ]

      proof

        let A be Subset of TM such that (TM | A) is second-countable and A is finite-ind and ( ind A) <= 0 ;

        let F be finite Subset-Family of TM such that F is open and

         A110: F is Cover of A and

         A111: ( card F) <= 0 ;

        ( rng {} ) c= ( bool the carrier of TM) & ( dom {} ) = F by A111;

        then

        reconsider g = {} as Function of F, ( bool the carrier of TM) by FUNCT_2: 2;

        take g;

        F = {} by A111;

        hence thesis by A110;

      end;

      for n holds P[n] from NAT_1:sch 2( A109, A3);

      then P[( card F)];

      hence thesis by A1, A2, TOPDIM_1: 18;

    end;

    theorem :: TOPDIM_2:23

    for TM st TM is second-countable finite-ind & ( ind TM) <= n holds for F st F is open & F is Cover of TM holds ex G st G is open & G is Cover of TM & G is_finer_than F & ( card G) <= (( card F) * (n + 1)) & ( order G) <= n

    proof

      let TM such that

       A1: TM is second-countable finite-ind and

       A2: ( ind TM) <= n;

      reconsider I = n as Integer;

      consider G be finite Subset-Family of TM such that

       A3: G is Cover of TM and

       A4: G is finite-ind & ( ind G) <= 0 and

       A5: ( card G) <= (I + 1) and for a,b be Subset of TM st a in G & b in G & a meets b holds a = b by A1, A2, Th7;

      set cTM = the carrier of TM;

      let F be finite Subset-Family of TM such that

       A6: F is open and

       A7: F is Cover of TM;

      

       A8: ( card ((n + 1) * ( card F))) = ((n + 1) * ( card F));

      defpred P[ object, object] means for A be Subset of TM st A = $1 holds ex g be Function of F, ( bool cTM) st $2 = ( rng g) & ( rng g) is open & ( rng g) is Cover of A & (for a be set st a in F holds (g . a) c= a) & for a,b be set st a in F & b in F & a <> b holds (g . a) misses (g . b);

      

       A9: for x be object st x in G holds ex y be object st y in ( bool ( bool cTM)) & P[x, y]

      proof

        let x be object;

        assume

         A10: x in G;

        then

        reconsider A = x as Subset of TM;

        

         A11: (TM | A) is second-countable by A1;

        ( [#] TM) c= ( union F) by A7, SETFAM_1:def 11;

        then A c= ( union F);

        then

         A12: F is Cover of A by SETFAM_1:def 11;

        A is finite-ind & ( ind A) <= 0 by A4, A10, TOPDIM_1: 11;

        then

        consider g be Function of F, ( bool the carrier of TM) such that

         A13: ( rng g) is open & ( rng g) is Cover of A & ((for a be set st a in F holds (g . a) c= a) & for a,b be set st a in F & b in F & a <> b holds (g . a) misses (g . b)) by A6, A11, A12, Th22;

        take ( rng g);

        thus thesis by A13;

      end;

      consider GG be Function of G, ( bool ( bool cTM)) such that

       A14: for x be object st x in G holds P[x, (GG . x)] from FUNCT_2:sch 1( A9);

      ( union ( rng GG)) c= ( union ( bool ( bool cTM))) by ZFMISC_1: 77;

      then

      reconsider Ugg = ( Union GG) as Subset-Family of TM;

      

       A15: ( dom GG) = G by FUNCT_2:def 1;

      

       A16: for x be object st x in ( dom GG) holds ( card (GG . x)) c= ( card F)

      proof

        let x be object;

        assume

         A17: x in ( dom GG);

        then

        reconsider A = x as Subset of TM by A15;

        consider g be Function of F, ( bool cTM) such that

         A18: (GG . x) = ( rng g) and ( rng g) is open and ( rng g) is Cover of A and for a be set st a in F holds (g . a) c= a and for a,b be set st a in F & b in F & a <> b holds (g . a) misses (g . b) by A14, A17;

        ( dom g) = F by FUNCT_2:def 1;

        hence thesis by A18, CARD_1: 12;

      end;

      ( Segm ( card ( dom GG))) c= ( Segm (n + 1)) by A5, A15, NAT_1: 39;

      then

       A19: ( card Ugg) c= ((n + 1) *` ( card F)) by A16, CARD_2: 86;

      ( card ( card F)) = ( card F) & ( card (n + 1)) = (n + 1);

      then

       A20: ((n + 1) *` ( card F)) = ((n + 1) * ( card F)) by A8, CARD_2: 39;

      then

      reconsider Ugg as finite Subset-Family of TM by A19;

      take Ugg;

      thus Ugg is open

      proof

        let A be Subset of TM;

        assume A in Ugg;

        then

        consider Y be set such that

         A21: A in Y and

         A22: Y in ( rng GG) by TARSKI:def 4;

        consider x be object such that

         A23: x in ( dom GG) & Y = (GG . x) by A22, FUNCT_1:def 3;

        reconsider x as set by TARSKI: 1;

        ex g be Function of F, ( bool cTM) st Y = ( rng g) & ( rng g) is open & ( rng g) is Cover of x & (for a be set st a in F holds (g . a) c= a) & for a,b be set st a in F & b in F & a <> b holds (g . a) misses (g . b) by A14, A15, A23;

        hence thesis by A21;

      end;

      ( [#] TM) c= ( union Ugg)

      proof

        

         A24: ( [#] TM) c= ( union G) by A3, SETFAM_1:def 11;

        let x be object such that

         A25: x in ( [#] TM);

        consider A be set such that

         A26: x in A and

         A27: A in G by A24, A25, TARSKI:def 4;

        consider g be Function of F, ( bool cTM) such that

         A28: (GG . A) = ( rng g) and ( rng g) is open and

         A29: ( rng g) is Cover of A and for a be set st a in F holds (g . a) c= a and for a,b be set st a in F & b in F & a <> b holds (g . a) misses (g . b) by A14, A27;

        A c= ( union ( rng g)) by A29, SETFAM_1:def 11;

        then

        consider y be set such that

         A30: x in y and

         A31: y in ( rng g) by A26, TARSKI:def 4;

        (GG . A) in ( rng GG) by A15, A27, FUNCT_1:def 3;

        then y in Ugg by A28, A31, TARSKI:def 4;

        hence thesis by A30, TARSKI:def 4;

      end;

      hence Ugg is Cover of TM by SETFAM_1:def 11;

      thus Ugg is_finer_than F

      proof

        let A be set;

        assume A in Ugg;

        then

        consider Y be set such that

         A32: A in Y and

         A33: Y in ( rng GG) by TARSKI:def 4;

        consider x be object such that

         A34: x in ( dom GG) & Y = (GG . x) by A33, FUNCT_1:def 3;

        reconsider x as set by TARSKI: 1;

        consider g be Function of F, ( bool cTM) such that

         A35: Y = ( rng g) and ( rng g) is open and ( rng g) is Cover of x and

         A36: for a be set st a in F holds (g . a) c= a and for a,b be set st a in F & b in F & a <> b holds (g . a) misses (g . b) by A14, A15, A34;

        ( dom g) = F by FUNCT_2:def 1;

        then ex z be object st z in F & (g . z) = A by A32, A35, FUNCT_1:def 3;

        hence thesis by A36;

      end;

      ( Segm ( card Ugg)) c= ( Segm (( card F) * (n + 1))) by A19, A20;

      hence ( card Ugg) <= (( card F) * (n + 1)) by NAT_1: 39;

      defpred Q[ object, object] means $1 in (GG . $2);

      now

        let H be finite Subset-Family of TM such that

         A37: H c= Ugg and

         A38: ( card H) > (n + 1);

        H is non empty by A38;

        then

        consider XX be object such that

         A39: XX in H;

        

         A40: for x be object st x in H holds ex y be object st y in G & Q[x, y]

        proof

          let A be object;

          assume A in H;

          then

          consider Y be set such that

           A41: A in Y and

           A42: Y in ( rng GG) by A37, TARSKI:def 4;

          ex x be object st x in ( dom GG) & Y = (GG . x) by A42, FUNCT_1:def 3;

          hence thesis by A41;

        end;

        consider q be Function of H, G such that

         A43: for x be object st x in H holds Q[x, (q . x)] from FUNCT_2:sch 1( A40);

        ex y be object st y in G & Q[XX, y] by A40, A39;

        then

         A44: ( dom q) = H by FUNCT_2:def 1;

        assume ( meet H) is non empty;

        then

        consider x be object such that

         A45: x in ( meet H);

        for x1,x2 be object st x1 in ( dom q) & x2 in ( dom q) & (q . x1) = (q . x2) holds x1 = x2

        proof

          let x1,x2 be object such that

           A46: x1 in ( dom q) and

           A47: x2 in ( dom q) and

           A48: (q . x1) = (q . x2);

          reconsider x1, x2 as set by TARSKI: 1;

          x in x1 & x in x2 by A45, A46, A47, SETFAM_1:def 1;

          then

           A49: x1 meets x2 by XBOOLE_0: 3;

          (q . x1) in ( rng q) by A46, FUNCT_1:def 3;

          then (q . x1) in G;

          then

          consider g be Function of F, ( bool cTM) such that

           A50: (GG . (q . x1)) = ( rng g) and ( rng g) is open and ( rng g) is Cover of (q . x1) and for a be set st a in F holds (g . a) c= a and

           A51: for a,b be set st a in F & b in F & a <> b holds (g . a) misses (g . b) by A14;

          

           A52: ( dom g) = F by FUNCT_2:def 1;

          x2 in (GG . (q . x1)) by A43, A47, A48;

          then

           A53: ex y2 be object st y2 in F & x2 = (g . y2) by A50, A52, FUNCT_1:def 3;

          x1 in (GG . (q . x1)) by A43, A46;

          then ex y1 be object st y1 in F & x1 = (g . y1) by A50, A52, FUNCT_1:def 3;

          hence thesis by A49, A51, A53;

        end;

        then

         A54: q is one-to-one by FUNCT_1:def 4;

        ( rng q) c= G;

        then ( Segm ( card H)) c= ( Segm ( card G)) by A54, A44, CARD_1: 10;

        then ( card H) <= ( card G) by NAT_1: 39;

        hence contradiction by A5, A38, XXREAL_0: 2;

      end;

      hence thesis by Th3;

    end;

    theorem :: TOPDIM_2:24

    for TM st TM is finite-ind holds for A st ( ind (A ` )) <= n & (TM | (A ` )) is second-countable holds for A1,A2 be closed Subset of TM st A = (A1 \/ A2) holds ex X1,X2 be closed Subset of TM st ( [#] TM) = (X1 \/ X2) & A1 c= X1 & A2 c= X2 & (A1 /\ X2) = (A1 /\ A2) & (A1 /\ A2) = (X1 /\ A2) & ( ind ((X1 /\ X2) \ (A1 /\ A2))) <= (n - 1)

    proof

      let TM such that

       A1: TM is finite-ind;

      set cTM = ( [#] TM);

      let A such that

       A2: ( ind (A ` )) <= n and

       A3: (TM | (A ` )) is second-countable;

      let A1,A2 be closed Subset of TM such that

       A4: A = (A1 \/ A2);

      set A12 = (A1 /\ A2);

      set T912 = (TM | (cTM \ A12));

      

       A5: ( [#] T912) = (cTM \ A12) by PRE_TOPC:def 5;

      (A ` ) c= (cTM \ A12) by A4, XBOOLE_1: 29, XBOOLE_1: 34;

      then

      reconsider A19 = (A1 \ A12), A29 = (A2 \ A12), A9 = (A ` ) as Subset of T912 by A5, XBOOLE_1: 33;

      (A2 /\ ( [#] T912)) = ((A2 /\ cTM) \ A12) by A5, XBOOLE_1: 49

      .= A29 by XBOOLE_1: 28;

      then

      reconsider A29 as closed Subset of T912 by PRE_TOPC: 13;

      (A1 /\ ( [#] T912)) = ((A1 /\ cTM) \ A12) by A5, XBOOLE_1: 49

      .= A19 by XBOOLE_1: 28;

      then

      reconsider A19 as closed Subset of T912 by PRE_TOPC: 13;

      (A1 \ A2) = A19 by XBOOLE_1: 47;

      then A19 misses A2 by XBOOLE_1: 79;

      then

       A6: A19 misses A29 by XBOOLE_1: 36, XBOOLE_1: 63;

      

       A7: ( ind (A ` )) = ( ind A9) by A1, TOPDIM_1: 21;

      (T912 | A9) is second-countable by A3, METRIZTS: 9;

      then

      consider L be Subset of T912 such that

       A8: L separates (A19,A29) and

       A9: ( ind (L /\ A9)) <= (n - 1) by A1, A2, A6, A7, Th11;

      consider U,W be open Subset of T912 such that

       A10: A19 c= U and

       A11: A29 c= W and

       A12: U misses W and

       A13: L = ((U \/ W) ` ) by A8, METRIZTS:def 3;

      ( [#] T912) c= cTM by PRE_TOPC:def 4;

      then

      reconsider L9 = L, U9 = U, W9 = W as Subset of TM by XBOOLE_1: 1;

      

       A14: A1 = ((A1 \ A12) \/ A12) & A2 = ((A2 \ A12) \/ A12) by XBOOLE_1: 17, XBOOLE_1: 45;

      L misses A

      proof

        assume L meets A;

        then

        consider x be object such that

         A15: x in L and

         A16: x in A by XBOOLE_0: 3;

        

         A17: x in A1 or x in A2 by A4, A16, XBOOLE_0:def 3;

         not x in A12 by A5, A15, XBOOLE_0:def 5;

        then x in A19 or x in A29 by A17, XBOOLE_0:def 5;

        then x in (U \/ W) by A10, A11, XBOOLE_0:def 3;

        hence thesis by A13, A15, XBOOLE_0:def 5;

      end;

      

      then

       A18: L = (L9 \ A) by XBOOLE_1: 83

      .= ((L /\ cTM) \ A) by XBOOLE_1: 28

      .= (L /\ A9) by XBOOLE_1: 49;

      

       A19: (cTM \ (cTM \ A12)) = (cTM /\ A12) by XBOOLE_1: 48

      .= A12 by XBOOLE_1: 28;

      

       A20: (A1 \ (A1 \ A12)) = (A1 /\ A12) by XBOOLE_1: 48

      .= A12 by XBOOLE_1: 17, XBOOLE_1: 28;

      (A12 ` ) is open;

      then

      reconsider U9, W9 as open Subset of TM by A5, TSEP_1: 9;

      take X2 = (W9 ` ), X1 = (U9 ` );

      

       A21: W9 c= X1 by A12, SUBSET_1: 23;

      

       A22: (W \/ (cTM \ (U \/ W))) = (W \/ (X1 /\ X2)) by XBOOLE_1: 53

      .= ((W9 \/ X1) /\ (W \/ X2)) by XBOOLE_1: 24

      .= ((W9 \/ X1) /\ cTM) by XBOOLE_1: 45

      .= (X1 /\ cTM) by A21, XBOOLE_1: 12

      .= X1 by XBOOLE_1: 28;

      

      thus (X2 \/ X1) = (cTM \ (U9 /\ W9)) by XBOOLE_1: 54

      .= (cTM \ {} ) by A12

      .= cTM;

      

       A23: U9 c= X2 by A12, SUBSET_1: 23;

      

       A24: (U \/ (cTM \ (U \/ W))) = (U \/ (X1 /\ X2)) by XBOOLE_1: 53

      .= ((U9 \/ X1) /\ (U \/ X2)) by XBOOLE_1: 24

      .= (cTM /\ (U \/ X2)) by XBOOLE_1: 45

      .= (cTM /\ X2) by A23, XBOOLE_1: 12

      .= X2 by XBOOLE_1: 28;

      (cTM \ (cTM \ A12)) c= (cTM \ (U \/ W)) by A5, XBOOLE_1: 34;

      hence

       A25: A1 c= X2 & A2 c= X1 by A10, A11, A14, A19, A24, A22, XBOOLE_1: 13;

      then

       A26: A12 c= (A1 /\ X1) by XBOOLE_1: 26;

      (A1 /\ X1) = ((cTM /\ A1) \ U9) by XBOOLE_1: 49

      .= (A1 \ U9) by XBOOLE_1: 28;

      then (A1 /\ X1) c= A12 by A10, A20, XBOOLE_1: 34;

      hence (A1 /\ X1) = A12 by A26;

      

       A27: (A2 \ (A2 \ A12)) = (A2 /\ A12) by XBOOLE_1: 48

      .= A12 by XBOOLE_1: 17, XBOOLE_1: 28;

      

       A28: A12 c= (A2 /\ X2) by A25, XBOOLE_1: 26;

      (A2 /\ X2) = ((cTM /\ A2) \ W9) by XBOOLE_1: 49

      .= (A2 \ W9) by XBOOLE_1: 28;

      then (A2 /\ X2) c= A12 by A11, A27, XBOOLE_1: 34;

      hence A12 = (X2 /\ A2) by A28;

      ((X2 /\ X1) \ A12) = ((cTM \ (W9 \/ U9)) \ A12) by XBOOLE_1: 53

      .= (cTM \ ((W9 \/ U9) \/ A12)) by XBOOLE_1: 41

      .= L by A5, A13, XBOOLE_1: 41;

      hence thesis by A1, A9, A18, TOPDIM_1: 21;

    end;