pcomps_2.miz



    begin

    reserve i for Nat;

    begin

    reserve R for Relation;

    reserve A for set;

    theorem :: PCOMPS_2:1

    

     Th1: R well_orders A implies (R |_2 A) well_orders A & A = ( field (R |_2 A))

    proof

      assume

       A1: R well_orders A;

      then

       A2: R is_reflexive_in A;

      

       A3: (R |_2 A) is_reflexive_in A

      proof

        let x be object;

        assume x in A;

        then [x, x] in R & [x, x] in [:A, A:] by A2, ZFMISC_1: 87;

        hence thesis by XBOOLE_0:def 4;

      end;

      

       A4: (R |_2 A) is_connected_in A

      proof

        let x,y be object;

        assume that

         A5: x in A & y in A and

         A6: x <> y;

        

         A7: R is_connected_in A by A1;

        now

          per cases by A5, A6, A7;

            case

             A8: [x, y] in R;

             [x, y] in [:A, A:] by A5, ZFMISC_1: 87;

            hence [x, y] in (R |_2 A) by A8, XBOOLE_0:def 4;

          end;

            case

             A9: [y, x] in R;

             [y, x] in [:A, A:] by A5, ZFMISC_1: 87;

            hence [y, x] in (R |_2 A) by A9, XBOOLE_0:def 4;

          end;

        end;

        hence thesis;

      end;

      

       A10: (R |_2 A) c= R by XBOOLE_1: 17;

      

       A11: (R |_2 A) is_antisymmetric_in A

      proof

        let x,y be object;

        assume

         A12: x in A & y in A & [x, y] in (R |_2 A) & [y, x] in (R |_2 A);

        R is_antisymmetric_in A by A1;

        hence thesis by A10, A12;

      end;

      

       A13: (R |_2 A) is_well_founded_in A

      proof

        let Y be set;

        assume

         A14: Y c= A & Y <> {} ;

        R is_well_founded_in A by A1;

        then

        consider a be object such that

         A15: a in Y & (R -Seg a) misses Y by A14;

        ((R |_2 A) -Seg a) c= (R -Seg a) by WELLORD1: 14;

        hence thesis by A15, XBOOLE_1: 63;

      end;

      

       A16: A c= ( field (R |_2 A))

      proof

        let x be object;

        assume x in A;

        then [x, x] in [:A, A:] & [x, x] in R by A2, ZFMISC_1: 87;

        then [x, x] in (R |_2 A) by XBOOLE_0:def 4;

        hence thesis by RELAT_1: 15;

      end;

      

       A17: (R |_2 A) is_transitive_in A

      proof

        let x,y,z be object;

        assume that

         A18: x in A and

         A19: y in A and

         A20: z in A and

         A21: [x, y] in (R |_2 A) & [y, z] in (R |_2 A);

        

         A22: [x, z] in [:A, A:] by A18, A20, ZFMISC_1: 87;

        R is_transitive_in A by A1;

        then [x, z] in R by A10, A18, A19, A20, A21;

        hence thesis by A22, XBOOLE_0:def 4;

      end;

      ( field (R |_2 A)) c= A by WELLORD1: 13;

      hence thesis by A16, A3, A17, A11, A4, A13;

    end;

    scheme :: PCOMPS_2:sch1

    MinSet { A() -> set , R() -> Relation , P[ object] } :

ex X be set st X in A() & P[X] & for Y be set st Y in A() & P[Y] holds [X, Y] in R()

      provided

       A1: R() well_orders A()

       and

       A2: ex X be set st X in A() & P[X];

      consider Y be set such that

       A3: for x be object holds x in Y iff x in A() & P[x] from XBOOLE_0:sch 1;

      

       A4: ex x be object st x in Y by A2, A3;

      for x be object holds x in Y implies x in A() by A3;

      then Y c= A();

      then

      consider X be object such that

       A5: X in Y and

       A6: for Z be object st Z in Y holds [X, Z] in R() by A1, A4, WELLORD1: 5;

      

       A7: for M be set st M in A() & P[M] holds [X, M] in R() by A3, A6;

      X in A() & P[X] by A3, A5;

      hence thesis by A7;

    end;

    definition

      let FX be set, R be Relation, B be Element of FX;

      :: PCOMPS_2:def1

      func PartUnion (B,R) -> set equals ( union (R -Seg B));

      coherence ;

    end

    definition

      let FX be set, R be Relation;

      :: PCOMPS_2:def2

      func DisjointFam (FX,R) -> set means A in it iff ex B be Element of FX st B in FX & A = (B \ ( PartUnion (B,R)));

      existence

      proof

        defpred P[ set] means ex B be Element of FX st B in FX & $1 = (B \ ( PartUnion (B,R)));

        consider X be set such that

         A1: for x be set holds x in X iff x in ( bool ( union FX)) & P[x] from XFAMILY:sch 1;

        reconsider X as set;

        take X;

        let A;

        thus A in X implies ex B be Element of FX st B in FX & A = (B \ ( PartUnion (B,R))) by A1;

        assume

         A2: ex B be Element of FX st B in FX & A = (B \ ( PartUnion (B,R)));

        then A c= ( union FX) by XBOOLE_1: 109, ZFMISC_1: 74;

        hence thesis by A1, A2;

      end;

      uniqueness

      proof

        defpred P[ object] means ex B be Element of FX st B in FX & $1 = (B \ ( PartUnion (B,R)));

        thus for X1,X2 be set st (for x be set holds x in X1 iff P[x]) & (for x be set holds x in X2 iff P[x]) holds X1 = X2 from XFAMILY:sch 3;

      end;

    end

    definition

      let X be set, n be Element of NAT , f be sequence of ( bool X);

      :: PCOMPS_2:def3

      func PartUnionNat (n,f) -> set equals ( union (f .: (( Seg n) \ {n})));

      coherence ;

    end

    begin

    reserve PT for non empty TopSpace;

    reserve PM for MetrSpace;

    reserve FX,GX,HX for Subset-Family of PT;

    reserve Y,V,W for Subset of PT;

    theorem :: PCOMPS_2:2

    

     Th2: PT is regular implies for FX st FX is Cover of PT & FX is open holds ex HX st HX is open & HX is Cover of PT & for V st V in HX holds ex W st W in FX & ( Cl V) c= W

    proof

      assume

       A1: PT is regular;

      let FX;

      assume that

       A2: FX is Cover of PT and

       A3: FX is open;

      defpred P[ set] means ex V1 be Subset of PT st V1 = $1 & V1 is open & ex W st W in FX & ( Cl V1) c= W;

      consider HX such that

       A4: for V be Subset of PT holds V in HX iff P[V] from SUBSET_1:sch 3;

      take HX;

      for V be Subset of PT st V in HX holds V is open

      proof

        let V be Subset of PT;

        assume V in HX;

        then ex V1 be Subset of PT st V1 = V & V1 is open & ex W st W in FX & ( Cl V1) c= W by A4;

        hence thesis;

      end;

      hence HX is open by TOPS_2:def 1;

      the carrier of PT c= ( union HX)

      proof

        let x be object;

        assume x in the carrier of PT;

        then

        reconsider x as Point of PT;

        consider V be Subset of PT such that

         A5: x in V and

         A6: V in FX by A2, PCOMPS_1: 3;

        reconsider V as Subset of PT;

        now

          per cases ;

            suppose

             A7: (V ` ) <> {} ;

            V is open by A3, A6, TOPS_2:def 1;

            then

             A8: (V ` ) is closed;

            x in ((V ` ) ` ) by A5;

            then

            consider X,Y be Subset of PT such that

             A9: X is open and

             A10: Y is open and

             A11: x in X and

             A12: (V ` ) c= Y and

             A13: X misses Y by A1, A7, A8, COMPTS_1:def 2;

            X c= (Y ` ) & (Y ` ) is closed by A10, A13, SUBSET_1: 23;

            then

             A14: ( Cl X) c= (Y ` ) by TOPS_1: 5;

            (Y ` ) c= V by A12, SUBSET_1: 17;

            then ( Cl X) c= V by A14;

            then X in HX by A4, A6, A9;

            hence x in ( union HX) by A11, TARSKI:def 4;

          end;

            suppose

             A15: (V ` ) = {} ;

            consider X be Subset of PT such that

             A16: X = ( [#] PT);

            

             A17: X is open by A16;

            V = (( {} PT) ` ) by A15

            .= ( [#] PT) by PRE_TOPC: 6;

            then ( Cl X) = V by A16, TOPS_1: 2;

            then X in HX by A4, A6, A17;

            hence x in ( union HX) by A16, TARSKI:def 4;

          end;

        end;

        hence thesis;

      end;

      hence HX is Cover of PT by SETFAM_1:def 11;

      let V be Subset of PT;

      assume V in HX;

      then ex V1 be Subset of PT st V1 = V & V1 is open & ex W st W in FX & ( Cl V1) c= W by A4;

      hence thesis;

    end;

    theorem :: PCOMPS_2:3

    for PT, FX st PT is T_2 & PT is paracompact & FX is Cover of PT & FX is open holds ex GX st GX is open & GX is Cover of PT & ( clf GX) is_finer_than FX & GX is locally_finite

    proof

      let PT, FX;

      assume that

       A1: PT is T_2 and

       A2: PT is paracompact and

       A3: FX is Cover of PT & FX is open;

      consider HX such that

       A4: HX is open & HX is Cover of PT and

       A5: for V st V in HX holds ex W st W in FX & ( Cl V) c= W by A1, A2, A3, Th2, PCOMPS_1: 24;

      consider GX such that

       A6: GX is open & GX is Cover of PT and

       A7: GX is_finer_than HX and

       A8: GX is locally_finite by A2, A4, PCOMPS_1:def 3;

      

       A9: for V st V in GX holds ex W st W in FX & ( Cl V) c= W

      proof

        let V;

        assume V in GX;

        then

        consider X be set such that

         A10: X in HX and

         A11: V c= X by A7;

        reconsider X as Subset of PT by A10;

        consider W such that

         A12: W in FX & ( Cl X) c= W by A5, A10;

        take W;

        ( Cl V) c= ( Cl X) by A11, PRE_TOPC: 19;

        hence thesis by A12;

      end;

      ( clf GX) is_finer_than FX

      proof

        let X be set;

        assume

         A13: X in ( clf GX);

        then

        reconsider X as Subset of PT;

        consider V such that

         A14: X = ( Cl V) and

         A15: V in GX by A13, PCOMPS_1:def 2;

        consider W such that

         A16: W in FX & ( Cl V) c= W by A9, A15;

        take W;

        thus thesis by A14, A16;

      end;

      hence thesis by A6, A8;

    end;

    theorem :: PCOMPS_2:4

    

     Th4: for f be Function of [:the carrier of PT, the carrier of PT:], REAL st f is_metric_of the carrier of PT holds PM = ( SpaceMetr (the carrier of PT,f)) implies the carrier of PM = the carrier of PT

    proof

      let f be Function of [:the carrier of PT, the carrier of PT:], REAL ;

      assume

       A1: f is_metric_of the carrier of PT;

      assume PM = ( SpaceMetr (the carrier of PT,f));

      then PM = MetrStruct (# the carrier of PT, f #) by A1, PCOMPS_1:def 7;

      hence thesis;

    end;

    theorem :: PCOMPS_2:5

    for f be Function of [:the carrier of PT, the carrier of PT:], REAL st f is_metric_of the carrier of PT holds PM = ( SpaceMetr (the carrier of PT,f)) implies (FX is Subset-Family of PT iff FX is Subset-Family of PM) by Th4;

    reserve Mn for Relation;

    reserve n,k,l,q,p,q1 for Nat;

    scheme :: PCOMPS_2:sch2

    XXX1 { PM() -> non empty set , UB() -> Subset-Family of PM() , F( object, object) -> Subset of PM() , P[ object], Q[ object, object, object, object] } :

ex f be sequence of ( bool ( bool PM())) st (f . 0 ) = UB() & for n be Nat holds (f . (n + 1)) = { ( union { F(c,n) where c be Element of PM() : for fq be Subset-Family of PM(), q st q <= n & fq = (f . q) holds Q[c, V, n, fq] }) where V be Subset of PM() : P[V] };

      reconsider A = <*UB()*> as Element of (( bool ( bool PM())) * ) by FINSEQ_1:def 11;

      defpred T[ Nat, FinSequence of ( bool ( bool PM())), set] means $3 = ($2 ^ <*{ ( union { F(c,$1) where c be Element of PM() : for fq be Subset-Family of PM(), q st q <= $1 & fq = ($2 /. (q + 1)) holds Q[c, V, $1, fq] }) where V be Subset of PM() : P[V] }*>);

      

       A1: for n be Nat holds for x be Element of (( bool ( bool PM())) * ) holds ex y be Element of (( bool ( bool PM())) * ) st T[n, x, y]

      proof

        let n be Nat;

        let x be Element of (( bool ( bool PM())) * );

        set T = { ( union { F(c,n) where c be Element of PM() : for fq be Subset-Family of PM(), q st q <= n & fq = (x /. (q + 1)) holds Q[c, V, n, fq] }) where V be Subset of PM() : P[V] };

        now

          let X be object;

          reconsider XX = X as set by TARSKI: 1;

          assume X in T;

          then

          consider V be Subset of PM() such that

           A2: X = ( union { F(c,n) where c be Element of PM() : for fq be Subset-Family of PM(), q st q <= n & fq = (x /. (q + 1)) holds Q[c, V, n, fq] }) and P[V];

          now

            let a be object;

            assume a in XX;

            then

            consider P be set such that

             A3: a in P and

             A4: P in { F(c,n) where c be Element of PM() : for fq be Subset-Family of PM(), q st q <= n & fq = (x /. (q + 1)) holds Q[c, V, n, fq] } by A2, TARSKI:def 4;

            ex c be Element of PM() st P = F(c,n) & for fq be Subset-Family of PM(), q st q <= n & fq = (x /. (q + 1)) holds Q[c, V, n, fq] by A4;

            hence a in PM() by A3;

          end;

          then XX c= PM();

          hence X in ( bool PM());

        end;

        then

        reconsider T as Subset-Family of PM() by TARSKI:def 3;

        reconsider T1 = <*T*> as FinSequence of ( bool ( bool PM()));

        consider y be FinSequence of ( bool ( bool PM())) such that

         A5: y = (x ^ T1);

        reconsider y as Element of (( bool ( bool PM())) * ) by FINSEQ_1:def 11;

        take y;

        thus thesis by A5;

      end;

      consider g be sequence of (( bool ( bool PM())) * ) such that

       A6: (g . 0 ) = A and

       A7: for n be Nat holds T[n, (g . n), (g . (n + 1))] from RECDEF_1:sch 2( A1);

      defpred R[ Nat] means ( len (g . $1)) = ($1 + 1);

      

       A8: for k st R[k] holds R[(k + 1)]

      proof

        let k such that

         A9: ( len (g . k)) = (k + 1);

        ( len (g . (k + 1))) = ( len ((g . k) ^ <*{ ( union { F(c,k) where c be Element of PM() : for fq be Subset-Family of PM(), q st q <= k & fq = ((g . k) /. (q + 1)) holds Q[c, V, k, fq] }) where V be Subset of PM() : P[V] }*>)) by A7

        .= (( len (g . k)) + 1) by FINSEQ_2: 16;

        hence thesis by A9;

      end;

      deffunc G( Nat) = ((g . $1) /. ( len (g . $1)));

      consider f be sequence of ( bool ( bool PM())) such that

       A10: for n be Element of NAT holds (f . n) = G(n) from FUNCT_2:sch 4;

      

       A11: for n be Nat holds (f . n) = G(n)

      proof

        let n be Nat;

        n in NAT by ORDINAL1:def 12;

        hence thesis by A10;

      end;

      take f;

      ( len <*UB()*>) = 1 by FINSEQ_1: 39;

      

      hence (f . 0 ) = ( <*UB()*> /. 1) by A6, A11

      .= UB() by FINSEQ_4: 16;

      let n be Nat;

      reconsider n as Element of NAT by ORDINAL1:def 12;

      defpred T[ Nat] means for q st q <= $1 holds (f . q) = ((g . $1) /. (q + 1));

      

       A12: R[ 0 ] by A6, FINSEQ_1: 39;

      

       A13: for n holds R[n] from NAT_1:sch 2( A12, A8);

      then

       A14: (( len (g . n)) + 1) = ((n + 1) + 1);

      

       A15: for k st T[k] holds T[(k + 1)]

      proof

        let k;

        assume

         A16: for q st q <= k holds (f . q) = ((g . k) /. (q + 1));

        let q;

        assume

         A17: q <= (k + 1);

        now

          per cases by A17, XXREAL_0: 1;

            suppose

             A18: q = (k + 1);

            

            thus (f . q) = ((g . q) /. ( len (g . q))) by A11

            .= ((g . (k + 1)) /. (q + 1)) by A13, A18;

          end;

            suppose

             A19: q < (k + 1);

            

             A20: (q + 1) >= 1 by NAT_1: 11;

            (q + 1) <= (k + 1) by A19, NAT_1: 13;

            then

             A21: (q + 1) in ( Seg (k + 1)) by A20, FINSEQ_1: 1;

            then (q + 1) in ( Seg ( len (g . k))) by A13;

            then

             A22: (q + 1) in ( dom (g . k)) by FINSEQ_1:def 3;

            

             A23: q <= k by A19, NAT_1: 13;

            ((k + 1) + 1) >= (k + 1) by NAT_1: 11;

            then ( Seg (k + 1)) c= ( Seg ((k + 1) + 1)) by FINSEQ_1: 5;

            then (q + 1) in ( Seg ((k + 1) + 1)) by A21;

            then (q + 1) in ( Seg ( len (g . (k + 1)))) by A13;

            then (q + 1) in ( dom (g . (k + 1))) by FINSEQ_1:def 3;

            

            hence ((g . (k + 1)) /. (q + 1)) = ((g . (k + 1)) . (q + 1)) by PARTFUN1:def 6

            .= (((g . k) ^ <*{ ( union { F(c,k) where c be Element of PM() : for fq be Subset-Family of PM(), q st q <= k & fq = ((g . k) /. (q + 1)) holds Q[c, V, k, fq] }) where V be Subset of PM() : P[V] }*>) . (q + 1)) by A7

            .= ((g . k) . (q + 1)) by A22, FINSEQ_1:def 7

            .= ((g . k) /. (q + 1)) by A22, PARTFUN1:def 6

            .= (f . q) by A16, A23;

          end;

        end;

        hence thesis;

      end;

      deffunc G2( set) = ( union { F(c,n) where c be Element of PM() : for fq be Subset-Family of PM(), q st q <= n & fq = ((g . n) /. (q + 1)) holds Q[c, $1, n, fq] });

      deffunc F2( set) = ( union { F(c,n) where c be Element of PM() : for fq be Subset-Family of PM(), q st q <= n & fq = (f . q) holds Q[c, $1, n, fq] });

      set NF = { F2(V) where V be Subset of PM() : P[V] };

      ( len (g . (n + 1))) = ((n + 1) + 1) by A13;

      then

       A24: ( dom (g . (n + 1))) = ( Seg ((n + 1) + 1)) by FINSEQ_1:def 3;

      

       A25: T[ 0 ]

      proof

        let q;

        assume q <= 0 ;

        then

         A26: q = 0 ;

        

        thus (f . q) = ((g . q) /. ( len (g . q))) by A11

        .= ((g . 0 ) /. (q + 1)) by A6, A26, FINSEQ_1: 39;

      end;

      

       A27: for n holds T[n] from NAT_1:sch 2( A25, A15);

      

       A28: for V be Subset of PM() st P[V] holds F2(V) = G2(V)

      proof

        deffunc F1( set) = F($1,n);

        let V be Subset of PM() such that P[V];

        defpred P1[ set] means for fq be Subset-Family of PM(), q st q <= n & fq = (f . q) holds Q[$1, V, n, fq];

        defpred P[ set] means for fq be Subset-Family of PM(), q st q <= n & fq = ((g . n) /. (q + 1)) holds Q[$1, V, n, fq];

        

         A29: for c be Element of PM() holds P1[c] iff P[c]

        proof

          let c be Element of PM();

          thus (for fq be Subset-Family of PM(), q st q <= n & fq = (f . q) holds Q[c, V, n, fq]) implies for fq be Subset-Family of PM(), q st q <= n & fq = ((g . n) /. (q + 1)) holds Q[c, V, n, fq]

          proof

            assume

             A30: for fq be Subset-Family of PM(), q st q <= n & fq = (f . q) holds Q[c, V, n, fq];

            let fq be Subset-Family of PM(), q;

            assume that

             A31: q <= n and

             A32: fq = ((g . n) /. (q + 1));

            fq = (f . q) by A27, A31, A32;

            hence thesis by A30, A31;

          end;

          assume

           A33: for fq be Subset-Family of PM(), q st q <= n & fq = ((g . n) /. (q + 1)) holds Q[c, V, n, fq];

          let fq be Subset-Family of PM(), q;

          assume that

           A34: q <= n and

           A35: fq = (f . q);

          (f . q) = ((g . n) /. (q + 1)) by A27, A34;

          hence thesis by A33, A34, A35;

        end;

        { F1(c) where c be Element of PM() : P1[c] } = { F1(c) where c be Element of PM() : P[c] } from FRAENKEL:sch 3( A29);

        hence thesis;

      end;

      

       A36: NF = { G2(V) where V be Subset of PM() : P[V] } from FRAENKEL:sch 6( A28);

      

      then

       A37: ( len (g . (n + 1))) = ( len ((g . n) ^ <*NF*>)) by A7

      .= (( len (g . n)) + 1) by FINSEQ_2: 16;

      reconsider n1 = (n + 1) as Element of NAT ;

      (f . n1) = G(n1) by A11

      .= ((g . n1) /. ( len (g . n1)))

      .= ((g . n1) /. (( len (g . n)) + 1)) by A37

      .= ((g . (n + 1)) . (( len (g . n)) + 1)) by A24, A14, FINSEQ_1: 4, PARTFUN1:def 6

      .= (((g . n) ^ <*NF*>) . (( len (g . n)) + 1)) by A7, A36

      .= NF by FINSEQ_1: 42;

      hence thesis;

    end;

    reconsider jd = (1 / 2) as Real;

    scheme :: PCOMPS_2:sch3

    XXX { PM() -> non empty set , UB() -> Subset-Family of PM() , F( object, object) -> Subset of PM() , P[ object], Q[ object, object, object] } :

ex f be sequence of ( bool ( bool PM())) st (f . 0 ) = UB() & for n be Nat holds (f . (n + 1)) = { ( union { F(c,n) where c be Element of PM() : Q[c, V, n] & not c in ( union { ( union (f . q)) : q <= n }) }) where V be Subset of PM() : P[V] };

      defpred Q1[ set, set, set, set] means Q[$1, $2, $3] & not $1 in ( union $4);

      consider f be sequence of ( bool ( bool PM())) such that

       A1: (f . 0 ) = UB() and

       A2: for n be Nat holds (f . (n + 1)) = { ( union { F(c,n) where c be Element of PM() : for fq be Subset-Family of PM(), q st q <= n & fq = (f . q) holds Q1[c, V, n, fq] }) where V be Subset of PM() : P[V] } from XXX1;

      take f;

      thus (f . 0 ) = UB() by A1;

      let n be Nat;

      deffunc F2( set) = ( union { F(c,n) where c be Element of PM() : for fq be Subset-Family of PM(), q st q <= n & fq = (f . q) holds Q[c, $1, n] & not c in ( union fq) });

      deffunc G2( set) = ( union { F(c,n) where c be Element of PM() : Q[c, $1, n] & not c in ( union { ( union (f . q)) : q <= n }) });

      set fxxx1 = { F2(V) where V be Subset of PM() : P[V] };

      set fxxx = { G2(V) where V be Subset of PM() : P[V] };

       A3:

      now

        deffunc F( set) = F($1,n);

        let V be Subset of PM();

        assume P[V];

        defpred P[ set] means for fq be Subset-Family of PM(), q st q <= n & fq = (f . q) holds Q[$1, V, n] & not $1 in ( union fq);

        defpred Q1[ set] means Q[$1, V, n] & not $1 in ( union { ( union (f . q1)) : q1 <= n });

         A4:

        now

          let c be Element of PM();

          

           A5: (for fq be Subset-Family of PM(), q st q <= n & fq = (f . q) holds not c in ( union fq)) iff not c in ( union { ( union (f . q)) : q <= n })

          proof

            thus (for fq be Subset-Family of PM(), q st q <= n & fq = (f . q) holds not c in ( union fq)) implies not c in ( union { ( union (f . q)) : q <= n })

            proof

              assume

               A6: for fq be Subset-Family of PM(), q st q <= n & fq = (f . q) holds not c in ( union fq);

              assume c in ( union { ( union (f . q)) : q <= n });

              then

              consider C be set such that

               A7: c in C and

               A8: C in { ( union (f . q)) : q <= n } by TARSKI:def 4;

              consider q be Nat such that

               A9: C = ( union (f . q)) & q <= n by A8;

              reconsider q as Element of NAT by ORDINAL1:def 12;

              (f . q) = (f . q);

              hence contradiction by A6, A7, A9;

            end;

            assume

             A10: not c in ( union { ( union (f . q)) : q <= n });

            let fq be Subset-Family of PM(), q;

            assume q <= n & fq = (f . q);

            then ( union fq) in { ( union (f . p)) : p <= n };

            hence thesis by A10, TARSKI:def 4;

          end;

          thus P[c] iff Q1[c]

          proof

            hereby

              reconsider q = n as Element of NAT by ORDINAL1:def 12;

              assume

               A11: for fq be Subset-Family of PM(), q st q <= n & fq = (f . q) holds Q[c, V, n] & not c in ( union fq);

              ex fq be Subset-Family of PM() st fq = (f . q);

              hence Q[c, V, n] by A11;

              thus not c in ( union { ( union (f . p)) : p <= n }) by A5, A11;

            end;

            assume Q[c, V, n] & not c in ( union { ( union (f . q)) : q <= n });

            hence thesis by A5;

          end;

        end;

        { F(c) where c be Element of PM() : P[c] } = { F(c) where c be Element of PM() : Q1[c] } from FRAENKEL:sch 3( A4);

        hence F2(V) = G2(V);

      end;

      fxxx1 = fxxx from FRAENKEL:sch 6( A3);

      hence thesis by A2;

    end;

    theorem :: PCOMPS_2:6

    

     Th6: PT is metrizable implies for FX be Subset-Family of PT st FX is Cover of PT & FX is open holds ex GX be Subset-Family of PT st GX is open & GX is Cover of PT & GX is_finer_than FX & GX is locally_finite

    proof

      assume PT is metrizable;

      then

      consider metr be Function of [:the carrier of PT, the carrier of PT:], REAL such that

       A1: metr is_metric_of the carrier of PT and

       A2: ( Family_open_set ( SpaceMetr (the carrier of PT,metr))) = the topology of PT by PCOMPS_1:def 8;

      let FX;

      consider R such that

       A3: R well_orders FX by WELLORD2: 17;

      defpred P1[ set] means $1 in FX;

      consider Mn such that

       A4: Mn = (R |_2 FX);

      assume that

       A5: FX is Cover of PT and

       A6: FX is open;

      consider PM be MetrSpace such that

       A7: PM = ( SpaceMetr (the carrier of PT,metr));

      reconsider PM as non empty MetrSpace by A1, A7, PCOMPS_1: 36;

      deffunc F1( Element of PM, Nat) = ( Ball ($1,(1 / (2 |^ ($2 + 1)))));

      set UB = { ( union { ( Ball (c,jd)) where c be Element of PM : c in (V \ ( PartUnion (V,Mn))) & ( Ball (c,(3 / 2))) c= V }) where V be Subset of PM : V in FX };

      UB is Subset-Family of PM

      proof

        reconsider UB as set;

        UB c= ( bool the carrier of PM)

        proof

          let x be object;

          reconsider xx = x as set by TARSKI: 1;

          assume x in UB;

          then

          consider V be Subset of PM such that

           A8: x = ( union { ( Ball (c,jd)) where c be Element of PM : c in (V \ ( PartUnion (V,Mn))) & ( Ball (c,(3 / 2))) c= V }) and V in FX;

          xx c= the carrier of PM

          proof

            let y be object;

            assume y in xx;

            then

            consider W be set such that

             A9: y in W and

             A10: W in { ( Ball (c,jd)) where c be Element of PM : c in (V \ ( PartUnion (V,Mn))) & ( Ball (c,(3 / 2))) c= V } by A8, TARSKI:def 4;

            ex c be Element of PM st W = ( Ball (c,jd)) & c in (V \ ( PartUnion (V,Mn))) & ( Ball (c,(3 / 2))) c= V by A10;

            hence thesis by A9;

          end;

          hence thesis;

        end;

        hence thesis;

      end;

      then

      reconsider UB as Subset-Family of PM;

      defpred Q1[ Element of PM, Subset of PM, Nat] means $1 in ($2 \ ( PartUnion ($2,Mn))) & ( Ball ($1,(3 / (2 |^ ($3 + 1))))) c= $2;

      consider f be sequence of ( bool ( bool the carrier of PM)) such that

       A11: (f . 0 ) = UB and

       A12: for n be Nat holds (f . (n + 1)) = { ( union { F1(c,n) where c be Element of PM : Q1[c, V, n] & not c in ( union { ( union (f . q)) : q <= n }) }) where V be Subset of PM : P1[V] } from XXX;

      defpred P2[ set] means ex n be Nat st $1 in (f . n);

      consider GX be Subset-Family of PM such that

       A13: for X be Subset of PM holds X in GX iff P2[X] from SUBSET_1:sch 3;

      reconsider GX as Subset-Family of PT by A1, A7, Th4;

      take GX;

      

       A14: for X be Subset of PT st X in GX holds X is open

      proof

        let X be Subset of PT;

        assume

         A15: X in GX;

        then

        reconsider X as Subset of PM;

        consider n be Nat such that

         A16: X in (f . n) by A13, A15;

        now

          per cases ;

            suppose

             A17: n = 0 ;

            thus X in the topology of PT

            proof

              consider V be Subset of PM such that

               A18: X = ( union { ( Ball (c,jd)) where c be Element of PM : c in (V \ ( PartUnion (V,Mn))) & ( Ball (c,(3 / 2))) c= V }) and V in FX by A11, A16, A17;

              set NF = { ( Ball (c,jd)) where c be Element of PM : c in (V \ ( PartUnion (V,Mn))) & ( Ball (c,(3 / 2))) c= V };

              NF c= ( bool the carrier of PM)

              proof

                let a be object;

                assume a in NF;

                then ex c be Element of PM st a = ( Ball (c,jd)) & c in (V \ ( PartUnion (V,Mn))) & ( Ball (c,(3 / 2))) c= V;

                hence thesis;

              end;

              then

              reconsider NF as Subset-Family of PM;

              NF c= ( Family_open_set PM)

              proof

                let a be object;

                assume a in NF;

                then ex c be Element of PM st a = ( Ball (c,jd)) & c in (V \ ( PartUnion (V,Mn))) & ( Ball (c,(3 / 2))) c= V;

                hence thesis by PCOMPS_1: 29;

              end;

              hence thesis by A2, A7, A18, PCOMPS_1: 32;

            end;

          end;

            suppose n > 0 ;

            then

            consider k be Nat such that

             A19: n = (k + 1) by NAT_1: 6;

            reconsider k as Element of NAT by ORDINAL1:def 12;

            thus X in the topology of PT

            proof

              X in { ( union { ( Ball (c,(1 / (2 |^ (k + 1))))) where c be Element of PM : c in (V \ ( PartUnion (V,Mn))) & ( Ball (c,(3 / (2 |^ (k + 1))))) c= V & not c in ( union { ( union (f . q)) where q be Nat : q <= k }) }) where V be Subset of PM : V in FX } by A12, A16, A19;

              then

              consider V be Subset of PM such that

               A20: X = ( union { ( Ball (c,(1 / (2 |^ (k + 1))))) where c be Element of PM : c in (V \ ( PartUnion (V,Mn))) & ( Ball (c,(3 / (2 |^ (k + 1))))) c= V & not c in ( union { ( union (f . q)) where q be Nat : q <= k }) }) and V in FX;

              reconsider NF = { ( Ball (c,(1 / (2 |^ (k + 1))))) where c be Element of PM : c in (V \ ( PartUnion (V,Mn))) & ( Ball (c,(3 / (2 |^ (k + 1))))) c= V & not c in ( union { ( union (f . q)) where q be Nat : q <= k }) } as set;

              NF c= ( bool the carrier of PM)

              proof

                let a be object;

                assume a in NF;

                then ex c be Element of PM st a = ( Ball (c,(1 / (2 |^ (k + 1))))) & c in (V \ ( PartUnion (V,Mn))) & ( Ball (c,(3 / (2 |^ (k + 1))))) c= V & not c in ( union { ( union (f . l)) : l <= k });

                hence thesis;

              end;

              then

              reconsider NF as Subset-Family of PM;

              NF c= ( Family_open_set PM)

              proof

                let a be object;

                assume a in NF;

                then ex c be Element of PM st a = ( Ball (c,(1 / (2 |^ (k + 1))))) & c in (V \ ( PartUnion (V,Mn))) & ( Ball (c,(3 / (2 |^ (k + 1))))) c= V & not c in ( union { ( union (f . l)) : l <= k });

                hence thesis by PCOMPS_1: 29;

              end;

              hence thesis by A2, A7, A20, PCOMPS_1: 32;

            end;

          end;

        end;

        hence thesis by PRE_TOPC:def 2;

      end;

      hence GX is open by TOPS_2:def 1;

      

       A21: Mn well_orders FX by A3, A4, Th1;

      the carrier of PT c= ( union GX)

      proof

        let x be object;

        defpred P1[ set] means x in $1;

        assume

         A22: x in the carrier of PT;

        then

        reconsider x9 = x as Element of PM by A1, A7, Th4;

        ex G be Subset of PT st x in G & G in FX by A5, A22, PCOMPS_1: 3;

        then

         A23: ex G be set st G in FX & P1[G];

        consider X be set such that

         A24: X in FX and

         A25: P1[X] and

         A26: for Y be set st Y in FX & P1[Y] holds [X, Y] in Mn from MinSet( A21, A23);

        reconsider X as Subset of PT by A24;

        X is open by A6, A24, TOPS_2:def 1;

        then

         A27: X in ( Family_open_set PM) by A2, A7, PRE_TOPC:def 2;

        reconsider X as Subset of PM by A1, A7, Th4;

        consider r be Real such that

         A28: r > 0 and

         A29: ( Ball (x9,r)) c= X by A25, A27, PCOMPS_1:def 4;

        defpred P2[ Nat] means (3 / (2 |^ $1)) <= r;

        ex k be Nat st P2[k] by A28, PREPOWER: 92;

        then

         A30: ex k be Nat st P2[k];

        consider k be Nat such that

         A31: P2[k] and for l be Nat st P2[l] holds k <= l from NAT_1:sch 5( A30);

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

        then (2 |^ k) > 0 & (2 |^ (k + 1)) >= (2 |^ k) by PREPOWER: 6, XREAL_1: 151;

        then

         A32: (3 / (2 |^ (k + 1))) <= (3 / (2 |^ k)) by XREAL_1: 118;

        assume

         A33: not x in ( union GX);

        

         A34: for V be set, n st V in (f . n) holds not x in V

        proof

          let V be set;

          let n;

          reconsider m = n as Element of NAT by ORDINAL1:def 12;

          

           A35: (f . m) in ( bool ( bool the carrier of PM));

          assume V in (f . n);

          then V in GX by A13, A35;

          hence thesis by A33, TARSKI:def 4;

        end;

        

         A36: for n holds not x in ( union (f . n))

        proof

          let n;

          assume x in ( union (f . n));

          then ex V be set st x in V & V in (f . n) by TARSKI:def 4;

          hence contradiction by A34;

        end;

        now

          set W = ( union { ( Ball (y,(1 / (2 |^ (k + 1))))) where y be Element of PM : y in (X \ ( PartUnion (X,Mn))) & ( Ball (y,(3 / (2 |^ (k + 1))))) c= X & not y in ( union { ( union (f . q)) where q be Nat : q <= k }) });

          

           A37: x in W

          proof

            

             A38: not x9 in ( union { ( union (f . q)) where q be Nat : q <= k })

            proof

              assume x9 in ( union { ( union (f . q)) where q be Nat : q <= k });

              then

              consider D be set such that

               A39: x9 in D and

               A40: D in { ( union (f . q)) where q be Nat : q <= k } by TARSKI:def 4;

              ex q be Nat st D = ( union (f . q)) & q <= k by A40;

              hence contradiction by A36, A39;

            end;

             not x9 in ( PartUnion (X,Mn))

            proof

              reconsider FX as set;

              assume x9 in ( PartUnion (X,Mn));

              then

              consider M be set such that

               A41: x9 in M and

               A42: M in (Mn -Seg X) by TARSKI:def 4;

              

               A43: M <> X by A42, WELLORD1: 1;

              

               A44: Mn is_antisymmetric_in FX by A21;

              

               A45: [M, X] in Mn by A42, WELLORD1: 1;

              then M in ( field Mn) by RELAT_1: 15;

              then

               A46: M in FX by A3, A4, Th1;

              then [X, M] in Mn by A26, A41;

              hence contradiction by A24, A43, A45, A46, A44;

            end;

            then

             A47: x9 in (X \ ( PartUnion (X,Mn))) by A25, XBOOLE_0:def 5;

            consider A be Subset of PM such that

             A48: A = ( Ball (x9,(1 / (2 |^ (k + 1)))));

             0 < (2 |^ (k + 1)) by PREPOWER: 6;

            then

             A49: x in A by A48, TBSP_1: 11, XREAL_1: 139;

            ( Ball (x9,(3 / (2 |^ (k + 1))))) c= ( Ball (x9,r)) by A31, A32, PCOMPS_1: 1, XXREAL_0: 2;

            then ( Ball (x9,(3 / (2 |^ (k + 1))))) c= X by A29;

            then A in { ( Ball (y,(1 / (2 |^ (k + 1))))) where y be Element of PM : y in (X \ ( PartUnion (X,Mn))) & ( Ball (y,(3 / (2 |^ (k + 1))))) c= X & not y in ( union { ( union (f . q)) where q be Nat : q <= k }) } by A48, A47, A38;

            hence thesis by A49, TARSKI:def 4;

          end;

          reconsider W as set;

          W in { ( union { ( Ball (y,(1 / (2 |^ (k + 1))))) where y be Element of PM : y in (V \ ( PartUnion (V,Mn))) & ( Ball (y,(3 / (2 |^ (k + 1))))) c= V & not y in ( union { ( union (f . q)) where q be Nat : q <= k }) }) where V be Subset of PM : V in FX } by A24;

          then W in (f . (k + 1)) by A12;

          hence ex W be set, l be Element of NAT st W in (f . l) & x in W by A37;

        end;

        hence contradiction by A34;

      end;

      hence

       A50: GX is Cover of PT by SETFAM_1:def 11;

      for X be set st X in GX holds ex Y be set st Y in FX & X c= Y

      proof

        let X be set;

        assume

         A51: X in GX;

        then

        reconsider X as Subset of PM;

        consider n be Nat such that

         A52: X in (f . n) by A13, A51;

        now

          per cases ;

            suppose

             A53: n = 0 ;

            thus ex Y be set st Y in FX & X c= Y

            proof

              consider V be Subset of PM such that

               A54: X = ( union { ( Ball (c,(1 / 2))) where c be Element of PM : c in (V \ ( PartUnion (V,Mn))) & ( Ball (c,(3 / 2))) c= V }) and

               A55: V in FX by A11, A52, A53;

              set NF = { ( Ball (c,(1 / 2))) where c be Element of PM : c in (V \ ( PartUnion (V,Mn))) & ( Ball (c,(3 / 2))) c= V };

              NF c= ( bool the carrier of PM)

              proof

                let a be object;

                assume a in NF;

                then ex c be Element of PM st a = ( Ball (c,(1 / 2))) & c in (V \ ( PartUnion (V,Mn))) & ( Ball (c,(3 / 2))) c= V;

                hence thesis;

              end;

              then

              reconsider NF as Subset-Family of PM;

              

               A56: for W be set st W in NF holds W c= V

              proof

                let W be set;

                assume W in NF;

                then

                consider c be Element of PM such that

                 A57: W = ( Ball (c,(1 / 2))) and c in (V \ ( PartUnion (V,Mn))) and

                 A58: ( Ball (c,(3 / 2))) c= V;

                ( Ball (c,(1 / 2))) c= ( Ball (c,(3 / 2))) by PCOMPS_1: 1;

                hence thesis by A57, A58;

              end;

              reconsider V as set;

              take Y = V;

              thus Y in FX by A55;

              thus thesis by A54, A56, ZFMISC_1: 76;

            end;

          end;

            suppose n > 0 ;

            then

            consider k be Nat such that

             A59: n = (k + 1) by NAT_1: 6;

            reconsider k as Element of NAT by ORDINAL1:def 12;

            thus ex Y be set st Y in FX & X c= Y

            proof

              X in { ( union { ( Ball (c,(1 / (2 |^ (k + 1))))) where c be Element of PM : c in (V \ ( PartUnion (V,Mn))) & ( Ball (c,(3 / (2 |^ (k + 1))))) c= V & not c in ( union { ( union (f . q)) where q be Nat : q <= k }) }) where V be Subset of PM : V in FX } by A12, A52, A59;

              then

              consider V be Subset of PM such that

               A60: X = ( union { ( Ball (c,(1 / (2 |^ (k + 1))))) where c be Element of PM : c in (V \ ( PartUnion (V,Mn))) & ( Ball (c,(3 / (2 |^ (k + 1))))) c= V & not c in ( union { ( union (f . q)) where q be Nat : q <= k }) }) and

               A61: V in FX;

              reconsider NF = { ( Ball (c,(1 / (2 |^ (k + 1))))) where c be Element of PM : c in (V \ ( PartUnion (V,Mn))) & ( Ball (c,(3 / (2 |^ (k + 1))))) c= V & not c in ( union { ( union (f . q)) where q be Nat : q <= k }) } as set;

              NF c= ( bool the carrier of PM)

              proof

                let a be object;

                assume a in NF;

                then ex c be Element of PM st a = ( Ball (c,(1 / (2 |^ (k + 1))))) & c in (V \ ( PartUnion (V,Mn))) & ( Ball (c,(3 / (2 |^ (k + 1))))) c= V & not c in ( union { ( union (f . q)) where q be Nat : q <= k });

                hence thesis;

              end;

              then

              reconsider NF as Subset-Family of PM;

              

               A62: for W be set st W in NF holds W c= V

              proof

                let W be set;

                assume W in NF;

                then

                consider c be Element of PM such that

                 A63: W = ( Ball (c,(1 / (2 |^ (k + 1))))) and c in (V \ ( PartUnion (V,Mn))) and

                 A64: ( Ball (c,(3 / (2 |^ (k + 1))))) c= V and not c in ( union { ( union (f . q)) where q be Nat : q <= k });

                ( Ball (c,(1 / (2 |^ (k + 1))))) c= ( Ball (c,(3 / (2 |^ (k + 1))))) by PCOMPS_1: 1, XREAL_1: 72;

                hence thesis by A63, A64;

              end;

              reconsider V as set;

              take Y = V;

              thus Y in FX by A61;

              thus thesis by A60, A62, ZFMISC_1: 76;

            end;

          end;

        end;

        hence thesis;

      end;

      hence GX is_finer_than FX;

      for x be Point of PT holds ex W be Subset of PT st x in W & W is open & { V : V in GX & V meets W } is finite

      proof

        let x be Point of PT;

        reconsider x9 = x as Element of PM by A1, A7, Th4;

        consider X be Subset of PT such that

         A65: x in X and

         A66: X in GX by A50, PCOMPS_1: 3;

        reconsider X as Subset of PT;

        X is open by A14, A66;

        then X in ( Family_open_set PM) by A2, A7, PRE_TOPC:def 2;

        then

        consider r be Real such that

         A67: r > 0 and

         A68: ( Ball (x9,r)) c= X by A65, PCOMPS_1:def 4;

        consider m be Nat such that

         A69: (1 / (2 |^ m)) <= r by A67, PREPOWER: 92;

        defpred P3[ set] means X in (f . $1);

        ex n be Nat st P3[n] by A13, A66;

        then

         A70: ex n be Nat st P3[n];

        consider k be Nat such that

         A71: P3[k] and for l be Nat st P3[l] holds k <= l from NAT_1:sch 5( A70);

        consider W be Subset of PM such that

         A72: W = ( Ball (x9,(1 / (2 |^ (((m + 1) + k) + 1)))));

        reconsider W as Subset of PT by A1, A7, Th4;

        

         A73: { V : V in GX & V meets W } is finite

        proof

          defpred P4[ object, set] means $1 in (f . $2);

          set NZ = { V : V in GX & V meets W };

          

           A74: for p be object st p in NZ holds ex n be Nat st P4[p, n]

          proof

            let p be object;

            assume p in NZ;

            then ex V be Subset of PT st p = V & V in GX & V meets W;

            hence thesis by A13;

          end;

          consider g be Function such that

           A75: ( dom g) = NZ and

           A76: for y be object st y in NZ holds ex n be Nat st (g . y) = n & P4[y, n] & for t be Nat st P4[y, t] holds n <= t from TREES_2:sch 4( A74);

          

           A77: ( rng g) c= { i : i < (((m + 1) + k) + 1) }

          proof

            let t be object;

            assume t in ( rng g);

            then

            consider a be object such that

             A78: a in ( dom g) and

             A79: t = (g . a) by FUNCT_1:def 3;

            assume

             A80: not t in { i : i < (((m + 1) + k) + 1) };

            

             A81: ex n be Nat st (g . a) = n & a in (f . n) & for p be Nat st a in (f . p) holds n <= p by A75, A76, A78;

            then

            reconsider t as Element of NAT by A79, ORDINAL1:def 12;

            consider V such that

             A82: a = V and V in GX and

             A83: V meets W by A75, A78;

            consider y be object such that

             A84: y in V and

             A85: y in W by A83, XBOOLE_0: 3;

            

             A86: t >= (((m + 1) + k) + 1) by A80;

            now

              per cases ;

                suppose t = 0 ;

                hence contradiction by A80;

              end;

                suppose t > 0 ;

                then

                consider l be Nat such that

                 A87: t = (l + 1) by NAT_1: 6;

                reconsider l as Element of NAT by ORDINAL1:def 12;

                

                 A88: V in { ( union { ( Ball (c,(1 / (2 |^ (l + 1))))) where c be Element of PM : c in (Y \ ( PartUnion (Y,Mn))) & ( Ball (c,(3 / (2 |^ (l + 1))))) c= Y & not c in ( union { ( union (f . q)) where q be Nat : q <= l }) }) where Y be Subset of PM : Y in FX } by A12, A79, A81, A82, A87;

                (2 |^ t) >= (2 |^ (((m + 1) + k) + 1)) & (2 |^ (((m + 1) + k) + 1)) > 0 by A86, PREPOWER: 6, PREPOWER: 93;

                then

                 A89: (1 / (2 |^ (((m + 1) + k) + 1))) >= (1 / (2 |^ t)) by XREAL_1: 118;

                consider Y be Subset of PM such that

                 A90: V = ( union { ( Ball (c,(1 / (2 |^ (l + 1))))) where c be Element of PM : c in (Y \ ( PartUnion (Y,Mn))) & ( Ball (c,(3 / (2 |^ (l + 1))))) c= Y & not c in ( union { ( union (f . q)) where q be Nat : q <= l }) }) and Y in FX by A88;

                reconsider NF = { ( Ball (c,(1 / (2 |^ (l + 1))))) where c be Element of PM : c in (Y \ ( PartUnion (Y,Mn))) & ( Ball (c,(3 / (2 |^ (l + 1))))) c= Y & not c in ( union { ( union (f . q)) where q be Nat : q <= l }) } as set;

                consider T be set such that

                 A91: y in T and

                 A92: T in NF by A84, A90, TARSKI:def 4;

                reconsider y as Element of PM by A85;

                consider c be Element of PM such that

                 A93: T = ( Ball (c,(1 / (2 |^ (l + 1))))) and c in (Y \ ( PartUnion (Y,Mn))) and ( Ball (c,(3 / (2 |^ (l + 1))))) c= Y and

                 A94: not c in ( union { ( union (f . q)) where q be Nat : q <= l }) by A92;

                ( dist (c,y)) < (1 / (2 |^ t)) by A87, A91, A93, METRIC_1: 11;

                then ( dist (c,y)) < (1 / (2 |^ (((m + 1) + k) + 1))) by A89, XXREAL_0: 2;

                then

                 A95: (( dist (c,y)) + ( dist (y,x9))) < ((1 / (2 |^ (((m + 1) + k) + 1))) + ( dist (y,x9))) by XREAL_1: 6;

                

                 A96: for t be Element of NAT st t < l holds not c in ( union (f . t))

                proof

                  let t be Element of NAT ;

                  assume t < l;

                  then

                   A97: ( union (f . t)) in { ( union (f . q)) where q be Nat : q <= l };

                  assume c in ( union (f . t));

                  hence contradiction by A94, A97, TARSKI:def 4;

                end;

                

                 A98: ( dist (c,x9)) >= (1 / (2 |^ m))

                proof

                  assume not ( dist (c,x9)) >= (1 / (2 |^ m));

                  then ( dist (x9,c)) < r by A69, XXREAL_0: 2;

                  then c in ( Ball (x9,r)) by METRIC_1: 11;

                  then

                   A99: c in ( union (f . k)) by A71, A68, TARSKI:def 4;

                  

                   A100: k <> l

                  proof

                    assume k = l;

                    then ( union (f . k)) in { ( union (f . q)) where q be Nat : q <= l };

                    hence contradiction by A94, A99, TARSKI:def 4;

                  end;

                  l >= (k + (m + 1)) & (k + (m + 1)) >= k by A86, A87, NAT_1: 11, XREAL_1: 6;

                  then k <= l by XXREAL_0: 2;

                  then k in NAT & k < l by A100, ORDINAL1:def 12, XXREAL_0: 1;

                  hence contradiction by A96, A99;

                end;

                (( dist (c,y)) + ( dist (y,x9))) >= ( dist (c,x9)) by METRIC_1: 4;

                then (( dist (c,y)) + ( dist (y,x9))) >= (1 / (2 |^ m)) by A98, XXREAL_0: 2;

                then ((1 / (2 |^ (((m + 1) + k) + 1))) + ( dist (y,x9))) > (1 / (2 |^ m)) by A95, XXREAL_0: 2;

                then

                 A101: ( dist (y,x9)) >= ((1 / (2 |^ m)) - (1 / (2 |^ (((m + 1) + k) + 1)))) by XREAL_1: 19;

                ((2 |^ (1 + k)) * 2) >= 2 by PREPOWER: 11, XREAL_1: 151;

                then

                 A102: (((2 |^ (1 + k)) * 2) - 1) >= (2 - 1) by XREAL_1: 9;

                (2 |^ ((1 + k) + 1)) <> 0 by PREPOWER: 5;

                

                then ((1 / (2 |^ m)) - (1 / (2 |^ (((m + 1) + k) + 1)))) = (((1 * (2 |^ ((1 + k) + 1))) / ((2 |^ m) * (2 |^ ((1 + k) + 1)))) - (1 / (2 |^ (((m + 1) + k) + 1)))) by XCMPLX_1: 91

                .= (((1 * (2 |^ ((1 + k) + 1))) / (2 |^ (m + ((1 + k) + 1)))) - (1 / (2 |^ (((m + 1) + k) + 1)))) by NEWTON: 8

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

                .= ((((2 |^ (1 + k)) * 2) - 1) / (2 |^ (((m + 1) + k) + 1))) by XCMPLX_1: 120;

                then ((1 / (2 |^ m)) - (1 / (2 |^ (((m + 1) + k) + 1)))) >= (1 / (2 |^ (((m + 1) + k) + 1))) by A102, XREAL_1: 72;

                then ( dist (y,x9)) >= (1 / (2 |^ (((m + 1) + k) + 1))) by A101, XXREAL_0: 2;

                hence contradiction by A72, A85, METRIC_1: 11;

              end;

            end;

            hence contradiction;

          end;

          for x1,x2 be object st x1 in ( dom g) & x2 in ( dom g) & (g . x1) = (g . x2) holds x1 = x2

          proof

            let x1,x2 be object;

            assume that

             A103: x1 in ( dom g) and

             A104: x2 in ( dom g) and

             A105: (g . x1) = (g . x2);

            assume

             A106: x1 <> x2;

            reconsider x1, x2 as set by TARSKI: 1;

            ex V2 be Subset of PT st x2 = V2 & V2 in GX & V2 meets W by A75, A104;

            then

            consider w2 be object such that

             A107: w2 in W and

             A108: w2 in x2 by XBOOLE_0: 3;

            consider n1 be Nat such that

             A109: (g . x1) = n1 and

             A110: x1 in (f . n1) and for t be Nat st x1 in (f . t) holds n1 <= t by A75, A76, A103;

            ex V1 be Subset of PT st x1 = V1 & V1 in GX & V1 meets W by A75, A103;

            then

            consider w1 be object such that

             A111: w1 in W and

             A112: w1 in x1 by XBOOLE_0: 3;

            reconsider w1, w2 as Element of PM by A111, A107;

            

             A113: ex n2 be Nat st (g . x2) = n2 & x2 in (f . n2) & for t be Nat st x2 in (f . t) holds n2 <= t by A75, A76, A104;

            now

              per cases ;

                suppose

                 A114: n1 = 0 ;

                ((m + k) + 1) >= 1 by NAT_1: 11;

                then (2 |^ ((m + 1) + k)) >= (2 |^ 1) by PREPOWER: 93;

                then (2 |^ ((m + 1) + k)) >= 2;

                then

                 A115: (1 / (2 |^ ((m + 1) + k))) <= (1 / 2) by XREAL_1: 118;

                

                 A116: (2 / (2 |^ (((m + 1) + k) + 1))) = ((1 * 2) / ((2 |^ ((m + 1) + k)) * 2)) by NEWTON: 6

                .= (1 / (2 |^ ((m + 1) + k))) by XCMPLX_1: 91;

                (((1 / 2) + (1 / (2 |^ (((m + 1) + k) + 1)))) + ((1 / (2 |^ (((m + 1) + k) + 1))) + (1 / 2))) = (((1 + 1) / 2) + ((1 / (2 |^ (((m + 1) + k) + 1))) + (1 / (2 |^ (((m + 1) + k) + 1)))))

                .= ((2 / 2) + (2 / (2 |^ (((m + 1) + k) + 1)))) by XCMPLX_1: 62;

                then ((((1 / 2) + (1 / (2 |^ (((m + 1) + k) + 1)))) + ((1 / (2 |^ (((m + 1) + k) + 1))) + (1 / 2))) - (2 / 2)) = (1 / (2 |^ ((m + 1) + k))) by A116;

                then

                 A117: (((1 / 2) + (1 / (2 |^ (((m + 1) + k) + 1)))) + ((1 / (2 |^ (((m + 1) + k) + 1))) + (1 / 2))) <= ((2 / 2) + (1 / 2)) by A115, XREAL_1: 20;

                

                 A118: Mn is_connected_in FX by A21;

                

                 A119: ( dist (x9,w2)) < (1 / (2 |^ (((m + 1) + k) + 1))) by A72, A107, METRIC_1: 11;

                consider M1 be Subset of PM such that

                 A120: x1 = ( union { ( Ball (c,(1 / 2))) where c be Element of PM : c in (M1 \ ( PartUnion (M1,Mn))) & ( Ball (c,(3 / 2))) c= M1 }) and

                 A121: M1 in FX by A11, A110, A114;

                consider k1 be set such that

                 A122: w1 in k1 and

                 A123: k1 in { ( Ball (c,(1 / 2))) where c be Element of PM : c in (M1 \ ( PartUnion (M1,Mn))) & ( Ball (c,(3 / 2))) c= M1 } by A112, A120, TARSKI:def 4;

                consider c1 be Element of PM such that

                 A124: k1 = ( Ball (c1,(1 / 2))) and

                 A125: c1 in (M1 \ ( PartUnion (M1,Mn))) and

                 A126: ( Ball (c1,(3 / 2))) c= M1 by A123;

                

                 A127: ( dist (c1,w1)) < (1 / 2) by A122, A124, METRIC_1: 11;

                consider M2 be Subset of PM such that

                 A128: x2 = ( union { ( Ball (c,(1 / 2))) where c be Element of PM : c in (M2 \ ( PartUnion (M2,Mn))) & ( Ball (c,(3 / 2))) c= M2 }) and

                 A129: M2 in FX by A11, A105, A109, A113, A114;

                consider k2 be set such that

                 A130: w2 in k2 and

                 A131: k2 in { ( Ball (c,(1 / 2))) where c be Element of PM : c in (M2 \ ( PartUnion (M2,Mn))) & ( Ball (c,(3 / 2))) c= M2 } by A108, A128, TARSKI:def 4;

                consider c2 be Element of PM such that

                 A132: k2 = ( Ball (c2,(1 / 2))) and

                 A133: c2 in (M2 \ ( PartUnion (M2,Mn))) and

                 A134: ( Ball (c2,(3 / 2))) c= M2 by A131;

                ( dist (x9,c2)) <= (( dist (x9,w2)) + ( dist (w2,c2))) & ( dist (c1,x9)) <= (( dist (c1,w1)) + ( dist (w1,x9))) by METRIC_1: 4;

                then

                 A135: (( dist (c1,x9)) + ( dist (x9,c2))) <= ((( dist (c1,w1)) + ( dist (w1,x9))) + (( dist (x9,w2)) + ( dist (w2,c2)))) by XREAL_1: 7;

                ( dist (c1,c2)) <= (( dist (c1,x9)) + ( dist (x9,c2))) by METRIC_1: 4;

                then ( dist (c1,c2)) <= (( dist (c1,w1)) + (( dist (w1,x9)) + (( dist (x9,w2)) + ( dist (w2,c2))))) by A135, XXREAL_0: 2;

                then (( dist (c1,c2)) - (( dist (w1,x9)) + (( dist (x9,w2)) + ( dist (w2,c2))))) <= ( dist (c1,w1)) by XREAL_1: 20;

                then (( dist (c1,c2)) - (( dist (w1,x9)) + (( dist (x9,w2)) + ( dist (w2,c2))))) < (1 / 2) by A127, XXREAL_0: 2;

                then ( dist (c1,c2)) < ((1 / 2) + (( dist (w1,x9)) + (( dist (x9,w2)) + ( dist (w2,c2))))) by XREAL_1: 19;

                then ( dist (c1,c2)) < (( dist (w1,x9)) + ((1 / 2) + (( dist (x9,w2)) + ( dist (w2,c2)))));

                then

                 A136: (( dist (c1,c2)) - ((1 / 2) + (( dist (x9,w2)) + ( dist (w2,c2))))) < ( dist (w1,x9)) by XREAL_1: 19;

                ( dist (x9,w1)) < (1 / (2 |^ (((m + 1) + k) + 1))) by A72, A111, METRIC_1: 11;

                then (( dist (c1,c2)) - ((1 / 2) + (( dist (x9,w2)) + ( dist (w2,c2))))) < (1 / (2 |^ (((m + 1) + k) + 1))) by A136, XXREAL_0: 2;

                then ( dist (c1,c2)) < ((1 / (2 |^ (((m + 1) + k) + 1))) + ((1 / 2) + (( dist (x9,w2)) + ( dist (w2,c2))))) by XREAL_1: 19;

                then ( dist (c1,c2)) < (( dist (x9,w2)) + (( dist (w2,c2)) + ((1 / (2 |^ (((m + 1) + k) + 1))) + (1 / 2))));

                then (( dist (c1,c2)) - (( dist (w2,c2)) + ((1 / (2 |^ (((m + 1) + k) + 1))) + (1 / 2)))) < ( dist (x9,w2)) by XREAL_1: 19;

                then (( dist (c1,c2)) - (( dist (w2,c2)) + ((1 / (2 |^ (((m + 1) + k) + 1))) + (1 / 2)))) < (1 / (2 |^ (((m + 1) + k) + 1))) by A119, XXREAL_0: 2;

                then ( dist (c1,c2)) < ((1 / (2 |^ (((m + 1) + k) + 1))) + (( dist (w2,c2)) + ((1 / (2 |^ (((m + 1) + k) + 1))) + (1 / 2)))) by XREAL_1: 19;

                then ( dist (c1,c2)) < (( dist (w2,c2)) + ((1 / (2 |^ (((m + 1) + k) + 1))) + ((1 / (2 |^ (((m + 1) + k) + 1))) + (1 / 2))));

                then

                 A137: (( dist (c1,c2)) - ((1 / (2 |^ (((m + 1) + k) + 1))) + ((1 / (2 |^ (((m + 1) + k) + 1))) + (1 / 2)))) < ( dist (w2,c2)) by XREAL_1: 19;

                ( dist (c2,w2)) < (1 / 2) by A130, A132, METRIC_1: 11;

                then (( dist (c1,c2)) - ((1 / (2 |^ (((m + 1) + k) + 1))) + ((1 / (2 |^ (((m + 1) + k) + 1))) + (1 / 2)))) < (1 / 2) by A137, XXREAL_0: 2;

                then ( dist (c1,c2)) < ((1 / 2) + ((1 / (2 |^ (((m + 1) + k) + 1))) + ((1 / (2 |^ (((m + 1) + k) + 1))) + (1 / 2)))) by XREAL_1: 19;

                then

                 A138: ( dist (c1,c2)) < (3 / 2) by A117, XXREAL_0: 2;

                then

                 A139: c1 in ( Ball (c2,(3 / 2))) by METRIC_1: 11;

                

                 A140: M1 <> M2 by A106, A120, A128;

                

                 A141: c2 in ( Ball (c1,(3 / 2))) by A138, METRIC_1: 11;

                now

                  per cases by A121, A129, A118, A140;

                    suppose [M1, M2] in Mn;

                    then M1 in (Mn -Seg M2) by A140, WELLORD1: 1;

                    then c2 in ( PartUnion (M2,Mn)) by A126, A141, TARSKI:def 4;

                    hence contradiction by A133, XBOOLE_0:def 5;

                  end;

                    suppose [M2, M1] in Mn;

                    then M2 in (Mn -Seg M1) by A140, WELLORD1: 1;

                    then c1 in ( PartUnion (M1,Mn)) by A134, A139, TARSKI:def 4;

                    hence contradiction by A125, XBOOLE_0:def 5;

                  end;

                end;

                hence contradiction;

              end;

                suppose n1 > 0 ;

                then

                consider l be Nat such that

                 A142: n1 = (l + 1) by NAT_1: 6;

                reconsider l as Element of NAT by ORDINAL1:def 12;

                

                 A143: x1 in { ( union { ( Ball (c,(1 / (2 |^ (l + 1))))) where c be Element of PM : c in (M1 \ ( PartUnion (M1,Mn))) & ( Ball (c,(3 / (2 |^ (l + 1))))) c= M1 & not c in ( union { ( union (f . q)) where q be Nat : q <= l }) }) where M1 be Subset of PM : M1 in FX } by A12, A110, A142;

                

                 A144: ( dist (x9,w2)) < (1 / (2 |^ (((m + 1) + k) + 1))) by A72, A107, METRIC_1: 11;

                

                 A145: x2 in { ( union { ( Ball (c,(1 / (2 |^ (l + 1))))) where c be Element of PM : c in (M2 \ ( PartUnion (M2,Mn))) & ( Ball (c,(3 / (2 |^ (l + 1))))) c= M2 & not c in ( union { ( union (f . q)) where q be Nat : q <= l }) }) where M2 be Subset of PM : M2 in FX } by A12, A105, A109, A113, A142;

                

                 A146: (((1 / (2 |^ (l + 1))) + (1 / (2 |^ (((m + 1) + k) + 1)))) + ((1 / (2 |^ (((m + 1) + k) + 1))) + (1 / (2 |^ (l + 1))))) = (((1 / (2 |^ (l + 1))) + (1 / (2 |^ (l + 1)))) + ((1 / (2 |^ (((m + 1) + k) + 1))) + (1 / (2 |^ (((m + 1) + k) + 1)))))

                .= (((1 + 1) / (2 |^ (l + 1))) + ((1 / (2 |^ (((m + 1) + k) + 1))) + (1 / (2 |^ (((m + 1) + k) + 1))))) by XCMPLX_1: 62

                .= ((2 / (2 |^ (l + 1))) + (2 / (2 |^ (((m + 1) + k) + 1)))) by XCMPLX_1: 62;

                n1 in ( rng g) by A103, A109, FUNCT_1:def 3;

                then n1 in { i : i < (((m + 1) + k) + 1) } by A77;

                then

                 A147: ex i st n1 = i & i < (((m + 1) + k) + 1);

                then

                consider h be Nat such that

                 A148: (((m + 1) + k) + 1) = ((l + 1) + h) by A142, NAT_1: 10;

                h <> 0 by A142, A147, A148;

                then

                consider i be Nat such that

                 A149: h = (i + 1) by NAT_1: 6;

                ((l + 1) + i) >= (l + 1) by NAT_1: 11;

                then (2 |^ (l + 1)) > 0 & (2 |^ ((l + 1) + i)) >= (2 |^ (l + 1)) by PREPOWER: 6, PREPOWER: 93;

                then

                 A150: (1 / (2 |^ ((l + 1) + i))) <= (1 / (2 |^ (l + 1))) by XREAL_1: 118;

                (2 / (2 |^ (((m + 1) + k) + 1))) = ((1 * 2) / ((2 |^ ((l + 1) + i)) * 2)) by A148, A149, NEWTON: 6

                .= (1 / (2 |^ ((l + 1) + i))) by XCMPLX_1: 91;

                then ((((1 / (2 |^ (l + 1))) + (1 / (2 |^ (((m + 1) + k) + 1)))) + ((1 / (2 |^ (((m + 1) + k) + 1))) + (1 / (2 |^ (l + 1))))) - (2 / (2 |^ (l + 1)))) = (1 / (2 |^ ((l + 1) + i))) by A146;

                then (((1 / (2 |^ (l + 1))) + (1 / (2 |^ (((m + 1) + k) + 1)))) + ((1 / (2 |^ (((m + 1) + k) + 1))) + (1 / (2 |^ (l + 1))))) <= ((2 / (2 |^ (l + 1))) + (1 / (2 |^ (l + 1)))) by A150, XREAL_1: 20;

                then

                 A151: (((1 / (2 |^ (l + 1))) + (1 / (2 |^ (((m + 1) + k) + 1)))) + ((1 / (2 |^ (((m + 1) + k) + 1))) + (1 / (2 |^ (l + 1))))) <= ((2 + 1) / (2 |^ (l + 1))) by XCMPLX_1: 62;

                

                 A152: Mn is_connected_in FX by A21;

                consider M1 be Subset of PM such that

                 A153: x1 = ( union { ( Ball (c,(1 / (2 |^ (l + 1))))) where c be Element of PM : c in (M1 \ ( PartUnion (M1,Mn))) & ( Ball (c,(3 / (2 |^ (l + 1))))) c= M1 & not c in ( union { ( union (f . q)) where q be Nat : q <= l }) }) and

                 A154: M1 in FX by A143;

                reconsider NF = { ( Ball (c,(1 / (2 |^ (l + 1))))) where c be Element of PM : c in (M1 \ ( PartUnion (M1,Mn))) & ( Ball (c,(3 / (2 |^ (l + 1))))) c= M1 & not c in ( union { ( union (f . q)) where q be Nat : q <= l }) } as set;

                consider k1 be set such that

                 A155: w1 in k1 and

                 A156: k1 in NF by A112, A153, TARSKI:def 4;

                consider c1 be Element of PM such that

                 A157: k1 = ( Ball (c1,(1 / (2 |^ (l + 1))))) and

                 A158: c1 in (M1 \ ( PartUnion (M1,Mn))) and

                 A159: ( Ball (c1,(3 / (2 |^ (l + 1))))) c= M1 and not c1 in ( union { ( union (f . q)) where q be Nat : q <= l }) by A156;

                

                 A160: ( dist (c1,w1)) < (1 / (2 |^ (l + 1))) by A155, A157, METRIC_1: 11;

                consider M2 be Subset of PM such that

                 A161: x2 = ( union { ( Ball (c,(1 / (2 |^ (l + 1))))) where c be Element of PM : c in (M2 \ ( PartUnion (M2,Mn))) & ( Ball (c,(3 / (2 |^ (l + 1))))) c= M2 & not c in ( union { ( union (f . q)) where q be Nat : q <= l }) }) and

                 A162: M2 in FX by A145;

                

                 A163: M1 <> M2 by A106, A153, A161;

                reconsider NF = { ( Ball (c,(1 / (2 |^ (l + 1))))) where c be Element of PM : c in (M2 \ ( PartUnion (M2,Mn))) & ( Ball (c,(3 / (2 |^ (l + 1))))) c= M2 & not c in ( union { ( union (f . q)) where q be Nat : q <= l }) } as set;

                consider k2 be set such that

                 A164: w2 in k2 and

                 A165: k2 in NF by A108, A161, TARSKI:def 4;

                consider c2 be Element of PM such that

                 A166: k2 = ( Ball (c2,(1 / (2 |^ (l + 1))))) and

                 A167: c2 in (M2 \ ( PartUnion (M2,Mn))) and

                 A168: ( Ball (c2,(3 / (2 |^ (l + 1))))) c= M2 and not c2 in ( union { ( union (f . q)) where q be Nat : q <= l }) by A165;

                ( dist (x9,c2)) <= (( dist (x9,w2)) + ( dist (w2,c2))) & ( dist (c1,x9)) <= (( dist (c1,w1)) + ( dist (w1,x9))) by METRIC_1: 4;

                then

                 A169: (( dist (c1,x9)) + ( dist (x9,c2))) <= ((( dist (c1,w1)) + ( dist (w1,x9))) + (( dist (x9,w2)) + ( dist (w2,c2)))) by XREAL_1: 7;

                ( dist (c1,c2)) <= (( dist (c1,x9)) + ( dist (x9,c2))) by METRIC_1: 4;

                then ( dist (c1,c2)) <= (( dist (c1,w1)) + (( dist (w1,x9)) + (( dist (x9,w2)) + ( dist (w2,c2))))) by A169, XXREAL_0: 2;

                then (( dist (c1,c2)) - (( dist (w1,x9)) + (( dist (x9,w2)) + ( dist (w2,c2))))) <= ( dist (c1,w1)) by XREAL_1: 20;

                then (( dist (c1,c2)) - (( dist (w1,x9)) + (( dist (x9,w2)) + ( dist (w2,c2))))) < (1 / (2 |^ (l + 1))) by A160, XXREAL_0: 2;

                then ( dist (c1,c2)) < ((1 / (2 |^ (l + 1))) + (( dist (w1,x9)) + (( dist (x9,w2)) + ( dist (w2,c2))))) by XREAL_1: 19;

                then ( dist (c1,c2)) < (( dist (w1,x9)) + ((1 / (2 |^ (l + 1))) + (( dist (x9,w2)) + ( dist (w2,c2)))));

                then

                 A170: (( dist (c1,c2)) - ((1 / (2 |^ (l + 1))) + (( dist (x9,w2)) + ( dist (w2,c2))))) < ( dist (w1,x9)) by XREAL_1: 19;

                ( dist (x9,w1)) < (1 / (2 |^ (((m + 1) + k) + 1))) by A72, A111, METRIC_1: 11;

                then (( dist (c1,c2)) - ((1 / (2 |^ (l + 1))) + (( dist (x9,w2)) + ( dist (w2,c2))))) < (1 / (2 |^ (((m + 1) + k) + 1))) by A170, XXREAL_0: 2;

                then ( dist (c1,c2)) < ((1 / (2 |^ (((m + 1) + k) + 1))) + ((1 / (2 |^ (l + 1))) + (( dist (x9,w2)) + ( dist (w2,c2))))) by XREAL_1: 19;

                then ( dist (c1,c2)) < (( dist (x9,w2)) + (( dist (w2,c2)) + ((1 / (2 |^ (((m + 1) + k) + 1))) + (1 / (2 |^ (l + 1))))));

                then (( dist (c1,c2)) - (( dist (w2,c2)) + ((1 / (2 |^ (((m + 1) + k) + 1))) + (1 / (2 |^ (l + 1)))))) < ( dist (x9,w2)) by XREAL_1: 19;

                then (( dist (c1,c2)) - (( dist (w2,c2)) + ((1 / (2 |^ (((m + 1) + k) + 1))) + (1 / (2 |^ (l + 1)))))) < (1 / (2 |^ (((m + 1) + k) + 1))) by A144, XXREAL_0: 2;

                then ( dist (c1,c2)) < ((1 / (2 |^ (((m + 1) + k) + 1))) + (( dist (w2,c2)) + ((1 / (2 |^ (((m + 1) + k) + 1))) + (1 / (2 |^ (l + 1)))))) by XREAL_1: 19;

                then ( dist (c1,c2)) < (( dist (w2,c2)) + ((1 / (2 |^ (((m + 1) + k) + 1))) + ((1 / (2 |^ (((m + 1) + k) + 1))) + (1 / (2 |^ (l + 1))))));

                then

                 A171: (( dist (c1,c2)) - ((1 / (2 |^ (((m + 1) + k) + 1))) + ((1 / (2 |^ (((m + 1) + k) + 1))) + (1 / (2 |^ (l + 1)))))) < ( dist (w2,c2)) by XREAL_1: 19;

                ( dist (c2,w2)) < (1 / (2 |^ (l + 1))) by A164, A166, METRIC_1: 11;

                then (( dist (c1,c2)) - ((1 / (2 |^ (((m + 1) + k) + 1))) + ((1 / (2 |^ (((m + 1) + k) + 1))) + (1 / (2 |^ (l + 1)))))) < (1 / (2 |^ (l + 1))) by A171, XXREAL_0: 2;

                then ( dist (c1,c2)) < ((1 / (2 |^ (l + 1))) + ((1 / (2 |^ (((m + 1) + k) + 1))) + ((1 / (2 |^ (((m + 1) + k) + 1))) + (1 / (2 |^ (l + 1)))))) by XREAL_1: 19;

                then

                 A172: ( dist (c1,c2)) < (3 / (2 |^ (l + 1))) by A151, XXREAL_0: 2;

                then

                 A173: c1 in ( Ball (c2,(3 / (2 |^ (l + 1))))) by METRIC_1: 11;

                

                 A174: c2 in ( Ball (c1,(3 / (2 |^ (l + 1))))) by A172, METRIC_1: 11;

                now

                  per cases by A154, A162, A152, A163;

                    suppose [M1, M2] in Mn;

                    then M1 in (Mn -Seg M2) by A163, WELLORD1: 1;

                    then c2 in ( PartUnion (M2,Mn)) by A159, A174, TARSKI:def 4;

                    hence contradiction by A167, XBOOLE_0:def 5;

                  end;

                    suppose [M2, M1] in Mn;

                    then M2 in (Mn -Seg M1) by A163, WELLORD1: 1;

                    then c1 in ( PartUnion (M1,Mn)) by A168, A173, TARSKI:def 4;

                    hence contradiction by A158, XBOOLE_0:def 5;

                  end;

                end;

                hence contradiction;

              end;

            end;

            hence contradiction;

          end;

          then g is one-to-one by FUNCT_1:def 4;

          then

           A175: (NZ,( rng g)) are_equipotent by A75, WELLORD2:def 4;

          { i : i < (((m + 1) + k) + 1) } is finite

          proof

            { i : i < (((m + 1) + k) + 1) } c= ( { 0 } \/ ( Seg (((m + 1) + k) + 1)))

            proof

              let x be object;

              assume x in { i : i < (((m + 1) + k) + 1) };

              then

               A176: ex i be Nat st x = i & i < (((m + 1) + k) + 1);

              then

              reconsider x1 = x as Nat;

              now

                per cases ;

                  suppose x1 = 0 ;

                  hence x1 in { 0 } or x1 in ( Seg (((m + 1) + k) + 1)) by TARSKI:def 1;

                end;

                  suppose x1 > 0 ;

                  then ex l be Nat st x1 = (l + 1) by NAT_1: 6;

                  then x1 >= 1 by NAT_1: 11;

                  hence x1 in { 0 } or x1 in ( Seg (((m + 1) + k) + 1)) by A176, FINSEQ_1: 1;

                end;

              end;

              hence thesis by XBOOLE_0:def 3;

            end;

            hence thesis;

          end;

          hence thesis by A77, A175, CARD_1: 38;

        end;

        (2 |^ (((m + 1) + k) + 1)) > 0 by PREPOWER: 6;

        then

         A177: (1 / (2 |^ (((m + 1) + k) + 1))) > 0 by XREAL_1: 139;

        W in the topology of PT by A2, A7, A72, PCOMPS_1: 29;

        then W is open by PRE_TOPC:def 2;

        hence thesis by A177, A72, A73, TBSP_1: 11;

      end;

      hence GX is locally_finite by PCOMPS_1:def 1;

    end;

    theorem :: PCOMPS_2:7

    PT is metrizable implies PT is paracompact

    proof

      assume PT is metrizable;

      then for FX be Subset-Family of PT st FX is Cover of PT & FX is open holds ex GX be Subset-Family of PT st GX is open & GX is Cover of PT & GX is_finer_than FX & GX is locally_finite by Th6;

      hence thesis by PCOMPS_1:def 3;

    end;