compl_sp.miz

    begin

    reserve i,n,m for Nat,

x,y,X,Y for set,

r,s for Real;

    definition

      let M be non empty MetrStruct;

      let S be SetSequence of M;

      :: COMPL_SP:def1

      attr S is pointwise_bounded means

      : Def1: for i holds (S . i) is bounded;

    end

    registration

      let M be non empty Reflexive MetrStruct;

      cluster pointwise_bounded non-empty for SetSequence of M;

      existence

      proof

        consider x be object such that

         A1: x in the carrier of M by XBOOLE_0:def 1;

        reconsider x as Point of M by A1;

        reconsider X = {x} as Subset of M;

        take S = ( NAT --> X);

         A2:

        now

          let x1,x2 be Point of M such that

           A3: x1 in X and

           A4: x2 in X;



           A5: x2 = x by A4, TARSKI:def 1;

          x1 = x by A3, TARSKI:def 1;

          hence ( dist (x1,x2)) <= 1 by A5, METRIC_1: 1;

        end;

         A6:

        now

          let i;

          reconsider i9 = i as Element of NAT by ORDINAL1:def 12;

          (S . i9) = X by FUNCOP_1: 7;

          hence (S . i) is bounded by A2;

        end;

        for x be object st x in ( dom S) holds (S . x) is non empty by FUNCOP_1: 7;

        hence thesis by A6, FUNCT_1:def 9;

      end;

    end

    definition

      let M be Reflexive non empty MetrStruct;

      let S be SetSequence of M;

      :: COMPL_SP:def2

      func diameter S -> Real_Sequence means

      : Def2: for i holds (it . i) = ( diameter (S . i));

      existence

      proof

        defpred P[ object, object] means for i st i = $1 holds $2 = ( diameter (S . i));



         A1: for x be object st x in NAT holds ex y be object st y in REAL & P[x, y]

        proof

          let x be object;

          assume x in NAT ;

          then

          reconsider i = x as Nat;

          take ( diameter (S . i));

          thus thesis by XREAL_0:def 1;

        end;

        consider f be sequence of REAL such that

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

        take f;

        let i;

        i in NAT by ORDINAL1:def 12;

        hence thesis by A2;

      end;

      uniqueness

      proof

        let D1,D2 be Real_Sequence such that

         A3: for i holds (D1 . i) = ( diameter (S . i)) and

         A4: for i holds (D2 . i) = ( diameter (S . i));

        now

          let x be Element of NAT ;



          thus (D1 . x) = ( diameter (S . x)) by A3

          .= (D2 . x) by A4;

        end;

        hence thesis by FUNCT_2: 63;

      end;

    end

    theorem :: COMPL_SP:1



     Th1: for M be Reflexive non empty MetrStruct holds for S be pointwise_bounded SetSequence of M holds ( diameter S) is bounded_below

    proof

      let M be Reflexive non empty MetrStruct;

      let S be pointwise_bounded SetSequence of M;

      set d = ( diameter S);

      now

        let n be Nat;



         A1: ( diameter (S . n)) = (d . n) by Def2;

        (S . n) is bounded by Def1;

        then 0 <= (d . n) by A1, TBSP_1: 21;

        hence ( - 1) < (d . n) by XXREAL_0: 2;

      end;

      hence thesis by SEQ_2:def 4;

    end;

    registration

      let M be Reflexive non empty MetrStruct, S be SetSequence of M;

      cluster ( diameter S) -> real-valued;

      coherence ;

    end

    theorem :: COMPL_SP:2



     Th2: for M be Reflexive non empty MetrStruct holds for S be pointwise_bounded SetSequence of M st S is non-ascending holds ( diameter S) is bounded_above & ( diameter S) is non-increasing

    proof

      let M be Reflexive non empty MetrStruct;

      let S be pointwise_bounded SetSequence of M such that

       A1: S is non-ascending;

      set d = ( diameter S);

       A2:

      now

        let n be Nat;



         A3: ((d . 0 ) + 0 ) < ((d . 0 ) + 1) by XREAL_1: 8;



         A4: ( diameter (S . n)) = (d . n) by Def2;



         A5: ( diameter (S . 0 )) = (d . 0 ) by Def2;



         A6: (S . 0 ) is bounded by Def1;

        (S . n) c= (S . 0 ) by A1, PROB_1:def 4;

        then (d . n) <= (d . 0 ) by A6, A4, A5, TBSP_1: 24;

        hence (d . n) < ((d . 0 ) + 1) by A3, XXREAL_0: 2;

      end;

      now

        let m,n be Nat such that m in ( dom d) and n in ( dom d) and

         A7: m <= n;



         A8: (S . m) is bounded by Def1;



         A9: ( diameter (S . m)) = (d . m) by Def2;



         A10: ( diameter (S . n)) = (d . n) by Def2;

        (S . n) c= (S . m) by A1, A7, PROB_1:def 4;

        hence (d . n) <= (d . m) by A8, A10, A9, TBSP_1: 24;

      end;

      hence thesis by A2, SEQM_3:def 4, SEQ_2:def 3;

    end;

    theorem :: COMPL_SP:3

    for M be Reflexive non empty MetrStruct holds for S be pointwise_bounded SetSequence of M st S is non-descending holds ( diameter S) is non-decreasing

    proof

      let M be Reflexive non empty MetrStruct;

      let S be pointwise_bounded SetSequence of M such that

       A1: S is non-descending;

      set d = ( diameter S);

      now

        let m,n be Nat such that m in ( dom d) and n in ( dom d) and

         A2: m <= n;



         A3: (S . n) is bounded by Def1;



         A4: ( diameter (S . m)) = (d . m) by Def2;



         A5: ( diameter (S . n)) = (d . n) by Def2;

        (S . m) c= (S . n) by A1, A2, PROB_1:def 5;

        hence (d . n) >= (d . m) by A3, A5, A4, TBSP_1: 24;

      end;

      hence thesis by SEQM_3:def 3;

    end;

    theorem :: COMPL_SP:4



     Th4: for M be non empty Reflexive MetrStruct holds for S be pointwise_bounded SetSequence of M st S is non-ascending & ( lim ( diameter S)) = 0 holds for F be sequence of M st for i holds (F . i) in (S . i) holds F is Cauchy

    proof

      let M be non empty Reflexive MetrStruct;

      let S be pointwise_bounded SetSequence of M such that

       A1: S is non-ascending and

       A2: ( lim ( diameter S)) = 0 ;

      set d = ( diameter S);



       A3: d is non-increasing by A1, Th2;



       A4: d is bounded_below by Th1;

      let F be sequence of M such that

       A5: for i holds (F . i) in (S . i);

      let r;

      assume r > 0 ;

      then

      consider n be Nat such that

       A6: for m be Nat st n <= m holds |.((d . m) - 0 ).| < r by A2, A4, A3, SEQ_2:def 7;

      take n;

      let m1,m2 be Nat such that

       A7: n <= m1 and

       A8: n <= m2;



       A9: (S . m2) c= (S . n) by A1, A8, PROB_1:def 4;



       A10: (F . m2) in (S . m2) by A5;



       A11: (F . m1) in (S . m1) by A5;



       A12: |.((d . n) - 0 ).| < r by A6;



       A13: ( diameter (S . n)) = (d . n) by Def2;



       A14: (S . n) is bounded by Def1;

      then 0 <= (d . n) by A13, TBSP_1: 21;

      then

       A15: (d . n) < r by A12, ABSVALUE:def 1;

      (S . m1) c= (S . n) by A1, A7, PROB_1:def 4;

      then ( dist ((F . m1),(F . m2))) <= (d . n) by A9, A11, A10, A14, A13, TBSP_1:def 8;

      hence thesis by A15, XXREAL_0: 2;

    end;

    theorem :: COMPL_SP:5



     Th5: for M be Reflexive symmetric triangle non empty MetrStruct holds for p be Point of M holds 0 <= r implies ( diameter ( cl_Ball (p,r))) <= (2 * r)

    proof

      let M be Reflexive symmetric triangle non empty MetrStruct;

      let p be Point of M;



       A1: ( dist (p,p)) = 0 by METRIC_1: 1;

      assume 0 <= r;

      then

       A2: p in ( cl_Ball (p,r)) by A1, METRIC_1: 12;

       A3:

      now

        let x,y be Point of M such that

         A4: x in ( cl_Ball (p,r)) and

         A5: y in ( cl_Ball (p,r));



         A6: ( dist (x,p)) <= r by A4, METRIC_1: 12;



         A7: ( dist (x,y)) <= (( dist (x,p)) + ( dist (p,y))) by METRIC_1: 4;

        ( dist (p,y)) <= r by A5, METRIC_1: 12;

        then (( dist (x,p)) + ( dist (p,y))) <= (r + r) by A6, XREAL_1: 7;

        hence ( dist (x,y)) <= (2 * r) by A7, XXREAL_0: 2;

      end;

      ( cl_Ball (p,r)) is bounded by TOPREAL6: 59;

      hence thesis by A2, A3, TBSP_1:def 8;

    end;

    definition

      let M be MetrStruct;

      let U be Subset of M;

      :: COMPL_SP:def3

      attr U is open means U in ( Family_open_set M);

    end

    definition

      let M be MetrStruct;

      let A be Subset of M;

      :: COMPL_SP:def4

      attr A is closed means (A ` ) is open;

    end

    registration

      let M be MetrStruct;

      cluster empty -> open for Subset of M;

      coherence

      proof

        let S be Subset of M;



         A1: ( TopSpaceMetr M) = TopStruct (# the carrier of M, ( Family_open_set M) #);

        assume S is empty;

        then S in ( Family_open_set M) by A1, PRE_TOPC: 1;

        hence thesis;

      end;

      cluster empty -> closed for Subset of M;

      coherence

      proof

        let S be Subset of M;

        assume S is empty;

        then

         A2: ( [#] M) = (S ` );

        ( [#] M) in ( Family_open_set M) by PCOMPS_1: 30;

        then ( [#] M) is open;

        hence thesis by A2;

      end;

    end

    registration

      let M be non empty MetrStruct;

      cluster open non empty for Subset of M;

      existence

      proof

        ( [#] M) in ( Family_open_set M) by PCOMPS_1: 30;

        then ( [#] M) is open;

        hence thesis;

      end;

      cluster closed non empty for Subset of M;

      existence

      proof

        (( {} M) ` ) is closed;

        hence thesis;

      end;

    end

    theorem :: COMPL_SP:6



     Th6: for M be MetrStruct holds for A be Subset of M, A9 be Subset of ( TopSpaceMetr M) st A9 = A holds (A is open iff A9 is open) & (A is closed iff A9 is closed)

    proof

      let M be MetrStruct;

      let A be Subset of M, A9 be Subset of ( TopSpaceMetr M) such that

       A1: A9 = A;

      thus A is open implies A9 is open by A1, PRE_TOPC:def 2;

      thus A9 is open implies A is open by PRE_TOPC:def 2, A1;

      thus A is closed implies A9 is closed

      proof

        assume A is closed;

        then (A ` ) is open;

        then (A ` ) in ( Family_open_set M);

        then (A9 ` ) is open by A1, PRE_TOPC:def 2;

        hence thesis by TOPS_1: 3;

      end;

      assume A9 is closed;

      then (A ` ) in ( Family_open_set M) by A1, PRE_TOPC:def 2;

      then (A ` ) is open;

      hence thesis;

    end;

    definition

      let T be TopStruct;

      let S be SetSequence of T;

      :: COMPL_SP:def5

      attr S is open means for i holds (S . i) is open;

      :: COMPL_SP:def6

      attr S is closed means

      : Def6: for i holds (S . i) is closed;

    end



     Lm1: for T be TopSpace holds ex S be SetSequence of T st S is open & S is closed & (T is non empty implies S is non-empty)

    proof

      let T be TopSpace;

      take S = ( NAT --> ( [#] T));



       A1: for i holds (S . i) is closed by FUNCOP_1: 7, ORDINAL1:def 12;

      for i holds (S . i) is open by FUNCOP_1: 7, ORDINAL1:def 12;

      hence S is open & S is closed by A1;

      assume T is non empty;

      then for x be object st x in ( dom S) holds (S . x) is non empty by FUNCOP_1: 7;

      hence thesis by FUNCT_1:def 9;

    end;

    registration

      let T be TopSpace;

      cluster open for SetSequence of T;

      existence

      proof

        ex S be SetSequence of T st S is open & S is closed & (T is non empty implies S is non-empty) by Lm1;

        hence thesis;

      end;

      cluster closed for SetSequence of T;

      existence

      proof

        ex S be SetSequence of T st S is open & S is closed & (T is non empty implies S is non-empty) by Lm1;

        hence thesis;

      end;

    end

    registration

      let T be non empty TopSpace;

      cluster open non-empty for SetSequence of T;

      existence

      proof

        ex S be SetSequence of T st S is open & S is closed & (T is non empty implies S is non-empty) by Lm1;

        hence thesis;

      end;

      cluster closed non-empty for SetSequence of T;

      existence

      proof

        ex S be SetSequence of T st S is open & S is closed & (T is non empty implies S is non-empty) by Lm1;

        hence thesis;

      end;

    end

    definition

      let M be MetrStruct;

      let S be SetSequence of M;

      :: COMPL_SP:def7

      attr S is open means for i holds (S . i) is open;

      :: COMPL_SP:def8

      attr S is closed means

      : Def8: for i holds (S . i) is closed;

    end

    registration

      let M be non empty MetrSpace;

      cluster non-empty pointwise_bounded open for SetSequence of M;

      existence

      proof

        consider x be object such that

         A1: x in the carrier of M by XBOOLE_0:def 1;

        reconsider x as Point of M by A1;

        set B = ( Ball (x,1));

        take S = ( NAT --> B);

         A2:

        now

          let y be object;

          assume y in ( dom S);

          then

          reconsider n = y as Element of NAT ;



           A3: B = (S . n) by FUNCOP_1: 7;

          ( dist (x,x)) = 0 by METRIC_1: 1;

          hence (S . y) is non empty by A3, METRIC_1: 11;

        end;

         A4:

        now

          let i;

          i in NAT by ORDINAL1:def 12;

          then

           A5: (S . i) = B by FUNCOP_1: 7;

          B in ( Family_open_set M) by PCOMPS_1: 29;

          hence (S . i) is open by A5;

        end;

        for i holds (S . i) is bounded by FUNCOP_1: 7, ORDINAL1:def 12;

        hence thesis by A2, A4, FUNCT_1:def 9;

      end;

      cluster non-empty pointwise_bounded closed for SetSequence of M;

      existence

      proof

        consider x be object such that

         A6: x in the carrier of M by XBOOLE_0:def 1;

        reconsider x as Point of M by A6;

        set B = ( cl_Ball (x,1));

        take S = ( NAT --> B);

         A7:

        now

          let y be object;

          assume y in ( dom S);

          then

          reconsider n = y as Element of NAT ;



           A8: B = (S . n) by FUNCOP_1: 7;

          ( dist (x,x)) = 0 by METRIC_1: 1;

          hence (S . y) is non empty by A8, METRIC_1: 12;

        end;

         A9:

        now

          let i;

          i in NAT by ORDINAL1:def 12;

          then

           A10: (S . i) = B by FUNCOP_1: 7;

          (( [#] M) \ B) in ( Family_open_set M) by NAGATA_1: 14;

          then (B ` ) is open;

          hence (S . i) is closed by A10;

        end;

        now

          let i;



           A11: i in NAT by ORDINAL1:def 12;

          B is bounded by TOPREAL6: 59;

          hence (S . i) is bounded by A11, FUNCOP_1: 7;

        end;

        hence thesis by A7, A9, FUNCT_1:def 9;

      end;

    end

    theorem :: COMPL_SP:7



     Th7: for M be MetrStruct holds for S be SetSequence of M, S9 be SetSequence of ( TopSpaceMetr M) st S9 = S holds (S is open iff S9 is open) & (S is closed iff S9 is closed)

    proof

      let M be MetrStruct;

      let S be SetSequence of M, S9 be SetSequence of ( TopSpaceMetr M) such that

       A1: S9 = S;

      thus S is open implies S9 is open

      proof

        assume

         A2: S is open;

        let i;

        (S . i) is open by A2;

        hence thesis by A1, Th6;

      end;

      thus S9 is open implies S is open

      proof

        assume

         A3: S9 is open;

        let i;

        (S9 . i) is open by A3;

        hence thesis by A1, Th6;

      end;

      thus S is closed implies S9 is closed

      proof

        assume

         A4: S is closed;

        let i;

        (S . i) is closed by A4;

        hence thesis by A1, Th6;

      end;

      assume

       A5: S9 is closed;

      let i;

      (S9 . i) is closed by A5;

      hence thesis by A1, Th6;

    end;

    theorem :: COMPL_SP:8



     Th8: for M be Reflexive symmetric triangle non empty MetrStruct holds for S,CL be Subset of M st S is bounded holds for S9 be Subset of ( TopSpaceMetr M) st S = S9 & CL = ( Cl S9) holds CL is bounded & ( diameter S) = ( diameter CL)

    proof

      let M be Reflexive symmetric triangle non empty MetrStruct;

      let S,CL be Subset of M such that

       A1: S is bounded;

      set d = ( diameter S);

      set T = ( TopSpaceMetr M);

      let S9 be Subset of T such that

       A2: S = S9 and

       A3: CL = ( Cl S9);

      per cases ;

        suppose

         A4: S <> {} ;

         A5:

        now

          let x,y be Point of M such that

           A6: x in CL and

           A7: y in CL;

          reconsider X = x, Y = y as Point of T;

          set dxy = ( dist (x,y));

          set dd = (dxy - d);

          set dd2 = (dd / 2);

          set Bx = ( Ball (x,dd2));

          set By = ( Ball (y,dd2));

          reconsider BX = Bx, BY = By as Subset of T;

          assume ( dist (x,y)) > d;

          then dd > (d - d) by XREAL_1: 14;

          then

           A8: dd2 > ( 0 / 2) by XREAL_1: 74;

          By in ( Family_open_set M) by PCOMPS_1: 29;

          then

           A9: BY is open by PRE_TOPC:def 2;

          Bx in ( Family_open_set M) by PCOMPS_1: 29;

          then

           A10: BX is open by PRE_TOPC:def 2;

          ( dist (y,y)) = 0 by METRIC_1: 1;

          then Y in BY by A8, METRIC_1: 11;

          then BY meets S9 by A3, A7, A9, TOPS_1: 12;

          then

          consider y1 be object such that

           A11: y1 in BY and

           A12: y1 in S9 by XBOOLE_0: 3;

          ( dist (x,x)) = 0 by METRIC_1: 1;

          then X in BX by A8, METRIC_1: 11;

          then BX meets S9 by A3, A6, A10, TOPS_1: 12;

          then

          consider x1 be object such that

           A13: x1 in BX and

           A14: x1 in S9 by XBOOLE_0: 3;

          reconsider x1, y1 as Point of M by A13, A11;



           A15: ( dist (x,x1)) < dd2 by A13, METRIC_1: 11;

          ( dist (x1,y1)) <= d by A1, A2, A14, A12, TBSP_1:def 8;

          then

           A16: (( dist (x,x1)) + ( dist (x1,y1))) < (dd2 + d) by A15, XREAL_1: 8;



           A17: ( dist (y,y1)) < dd2 by A11, METRIC_1: 11;

          ( dist (x,y1)) <= (( dist (x,x1)) + ( dist (x1,y1))) by METRIC_1: 4;

          then ( dist (x,y1)) < (dd2 + d) by A16, XXREAL_0: 2;

          then (( dist (x,y1)) + ( dist (y1,y))) < ((dd2 + d) + dd2) by A17, XREAL_1: 8;

          hence contradiction by METRIC_1: 4;

        end;

         A18:

        now



           A19: (d + 0 ) < (d + 1) by XREAL_1: 8;

          let x,y be Point of M such that

           A20: x in CL and

           A21: y in CL;

          ( dist (x,y)) <= d by A5, A20, A21;

          hence ( dist (x,y)) <= (d + 1) by A19, XXREAL_0: 2;

        end;

         A22:

        now

          let s such that

           A23: for x,y be Point of M st x in CL & y in CL holds ( dist (x,y)) <= s;

          now

            let x,y be Point of M such that

             A24: x in S and

             A25: y in S;

            S c= CL by A2, A3, PRE_TOPC: 18;

            hence ( dist (x,y)) <= s by A23, A24, A25;

          end;

          hence d <= s by A1, A4, TBSP_1:def 8;

        end;



         A26: CL <> {} by A2, A3, A4, PCOMPS_1: 2;

        (d + 1) > ( 0 + 0 ) by A1, TBSP_1: 21, XREAL_1: 8;

        then CL is bounded by A18;

        hence thesis by A26, A5, A22, TBSP_1:def 8;

      end;

        suppose S = {} ;

        hence thesis by A2, A3, PCOMPS_1: 2;

      end;

    end;

    begin

    theorem :: COMPL_SP:9



     Th9: for M be non empty MetrSpace holds for C be sequence of M holds ex S be non-empty closed SetSequence of M st S is non-ascending & (C is Cauchy implies S is pointwise_bounded & ( lim ( diameter S)) = 0 ) & for i holds ex U be Subset of ( TopSpaceMetr M) st U = { (C . j) where j be Nat : j >= i } & (S . i) = ( Cl U)

    proof

      let M be Reflexive symmetric triangle non empty MetrSpace;

      set T = ( TopSpaceMetr M);

      let C be sequence of M;

      defpred P[ object, object] means for i st i = $1 holds ex S be Subset of T st S = { (C . j) where j be Nat : j >= i } & $2 = ( Cl S);



       A1: for x be object st x in NAT holds ex y be object st y in ( bool the carrier of M) & P[x, y]

      proof

        let x be object;

        assume x in NAT ;

        then

        reconsider x9 = x as Nat;

        set S = { (C . j) where j be Nat : j >= x9 };

        S c= the carrier of T

        proof

          let y be object;

          assume y in S;

          then ex j be Nat st (C . j) = y & j >= x9;

          hence thesis;

        end;

        then

        reconsider S as Subset of T;

        take ( Cl S);

        thus thesis;

      end;

      consider S be SetSequence of M such that

       A2: for x be object st x in NAT holds P[x, (S . x)] from FUNCT_2:sch 1( A1);

       A3:

      now

        let x be object;

        assume x in ( dom S);

        then

        reconsider i = x as Element of NAT ;

        consider U be Subset of T such that

         A4: U = { (C . j) where j be Nat : j >= i } and

         A5: (S . i) = ( Cl U) by A2;



         A6: U c= (S . i) by A5, PRE_TOPC: 18;

        (C . i) in U by A4;

        hence (S . x) is non empty by A6;

      end;

      now

        let i;

        i in NAT by ORDINAL1:def 12;

        then ex U be Subset of T st U = { (C . j) where j be Nat : j >= i } & (S . i) = ( Cl U) by A2;

        hence (S . i) is closed by Th6;

      end;

      then

      reconsider S as non-empty closed SetSequence of M by A3, Def8, FUNCT_1:def 9;

      take S;

      now

        let i be Nat;

        i in NAT by ORDINAL1:def 12;

        then

        consider U be Subset of T such that

         A7: U = { (C . j) where j be Nat : j >= i } and

         A8: (S . i) = ( Cl U) by A2;

        consider U1 be Subset of T such that

         A9: U1 = { (C . j) where j be Nat : j >= (i + 1) } and

         A10: (S . (i + 1)) = ( Cl U1) by A2;

        U1 c= U

        proof

          let x be object;

          assume x in U1;

          then

          consider j be Nat such that

           A11: x = (C . j) and

           A12: j >= (i + 1) by A9;

          j >= i by A12, NAT_1: 13;

          hence thesis by A7, A11;

        end;

        hence (S . (i + 1)) c= (S . i) by A8, A10, PRE_TOPC: 19;

      end;

      hence

       A13: S is non-ascending by KURATO_0:def 3;

      thus C is Cauchy implies S is pointwise_bounded & ( lim ( diameter S)) = 0

      proof

        assume

         A14: C is Cauchy;

         A15:

        now

          let i;

          i in NAT by ORDINAL1:def 12;

          then

          consider U be Subset of T such that

           A16: U = { (C . j) where j be Nat : j >= i } and

           A17: (S . i) = ( Cl U) by A2;

          reconsider U9 = U as Subset of M;

          U c= ( rng C)

          proof

            let x be object;

            assume x in U;

            then

            consider j be Nat such that

             A18: x = (C . j) & j >= i by A16;



             A19: j in NAT by ORDINAL1:def 12;

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

            hence thesis by A18, FUNCT_1:def 3, A19;

          end;

          then U9 is bounded by A14, TBSP_1: 14, TBSP_1: 26;

          hence (S . i) is bounded by A17, Th8;

        end;

        then

        reconsider S9 = S as non-empty pointwise_bounded closed SetSequence of M by Def1;

        set d = ( diameter S9);



         A20: for r be Real st 0 < r holds ex n be Nat st for m be Nat st n <= m holds |.((d . m) - 0 ).| < r

        proof

          let r be Real such that

           A21: 0 < r;

          reconsider R = r as Real;

          set R2 = (R / 2);

          R2 > 0 by A21, XREAL_1: 139;

          then

          consider p be Nat such that

           A22: for n,m be Nat st p <= n & p <= m holds ( dist ((C . n),(C . m))) < R2 by A14;

          take p;

          let m be Nat such that

           A23: p <= m;

          m in NAT by ORDINAL1:def 12;

          then

          consider U be Subset of T such that

           A24: U = { (C . j) where j be Nat : j >= m } and

           A25: (S . m) = ( Cl U) by A2;

          reconsider U9 = U as Subset of M;

           A26:

          now

            let x,y be Point of M such that

             A27: x in U9 and

             A28: y in U9;

            consider j be Nat such that

             A29: y = (C . j) and

             A30: j >= m by A24, A28;



             A31: j >= p by A23, A30, XXREAL_0: 2;

            consider i be Nat such that

             A32: x = (C . i) and

             A33: i >= m by A24, A27;

            i >= p by A23, A33, XXREAL_0: 2;

            hence ( dist (x,y)) <= R2 by A22, A32, A29, A31;

          end;



           A34: U c= ( rng C)

          proof

            let x be object;

            assume x in U;

            then

            consider j be Nat such that

             A35: x = (C . j) & j >= m by A24;



             A36: j in NAT by ORDINAL1:def 12;

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

            hence thesis by A35, FUNCT_1:def 3, A36;

          end;

          then

           A37: U9 is bounded by A14, TBSP_1: 14, TBSP_1: 26;

          then

           A38: ( diameter U9) = ( diameter (S . m)) by A25, Th8;

          (C . m) in U by A24;

          then

           A39: ( diameter U9) <= R2 by A37, A26, TBSP_1:def 8;

          ( rng C) is bounded by A14, TBSP_1: 26;

          then ( diameter (S . m)) >= 0 by A34, A38, TBSP_1: 14, TBSP_1: 21;

          then

           A40: |.( diameter (S . m)).| <= R2 by A39, A38, ABSVALUE:def 1;

          R2 < R by A21, XREAL_1: 216;

          then |.( diameter (S . m)).| < R by A40, XXREAL_0: 2;

          hence thesis by Def2;

        end;

        thus S is pointwise_bounded by A15;



         A41: d is bounded_below by Th1;

        d is non-increasing by A13, Th2;

        hence thesis by A41, A20, SEQ_2:def 7;

      end;

      let i;

      i in NAT by ORDINAL1:def 12;

      hence thesis by A2;

    end;

    theorem :: COMPL_SP:10



     Th10: for M be non empty MetrSpace holds M is complete iff for S be non-empty pointwise_bounded closed SetSequence of M st S is non-ascending & ( lim ( diameter S)) = 0 holds ( meet S) is non empty

    proof

      let M be non empty MetrSpace;

      set T = ( TopSpaceMetr M);

      thus M is complete implies for S be non-empty pointwise_bounded closed SetSequence of M st S is non-ascending & ( lim ( diameter S)) = 0 holds ( meet S) is non empty

      proof

        assume

         A1: M is complete;

        let S be non-empty pointwise_bounded closed SetSequence of M such that

         A2: S is non-ascending and

         A3: ( lim ( diameter S)) = 0 ;

        defpred P[ object, object] means $2 in (S . $1);



         A4: for x be object st x in NAT holds ex y be object st y in the carrier of M & P[x, y]

        proof



           A5: ( dom S) = NAT by FUNCT_2:def 1;

          let x be object such that

           A6: x in NAT ;

          (S . x) is non empty by A6, A5, FUNCT_1:def 9;

          then

           A7: ex y be object st y in (S . x) by XBOOLE_0:def 1;

          (S . x) in ( rng S) by A6, A5, FUNCT_1:def 3;

          hence thesis by A7;

        end;

        consider F be sequence of the carrier of M such that

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

        for i holds (F . i) in (S . i) by A8, ORDINAL1:def 12;

        then F is Cauchy by A2, A3, Th4;

        then F is convergent by A1;

        then

        consider x be Point of M such that

         A9: F is_convergent_in_metrspace_to x by METRIC_6: 10;

        reconsider F9 = F as sequence of T;

        reconsider x9 = x as Point of T;

        now

          let i be Nat;

          set F1 = (F9 ^\ i);

          reconsider Si = (S . i) as Subset of T;



           A10: ( rng F1) c= Si

          proof

            let x be object;

            assume x in ( rng F1);

            then

            consider y be object such that

             A11: y in ( dom F1) and

             A12: (F1 . y) = x by FUNCT_1:def 3;

            reconsider y as Element of NAT by A11;

            i <= (y + i) by NAT_1: 11;

            then

             A13: (S . (y + i)) c= (S . i) by A2, PROB_1:def 4;



             A14: (y + i) in NAT by ORDINAL1:def 12;

            x = (F . (y + i)) by A12, NAT_1:def 3;

            then x in (S . (y + i)) by A8, A14;

            hence thesis by A13;

          end;

          F9 is_convergent_to x9 by A9, FRECHET2: 28;

          then F1 is_convergent_to x9 by FRECHET2: 15;

          then

           A15: x in ( Lim F1) by FRECHET:def 5;

          (S . i) is closed by Def8;

          then Si is closed by Th6;

          then ( Lim F1) c= Si by A10, FRECHET2: 9;

          hence x in (S . i) by A15;

        end;

        hence thesis by KURATO_0: 3;

      end;

      assume

       A16: for S be non-empty pointwise_bounded closed SetSequence of M st S is non-ascending & ( lim ( diameter S)) = 0 holds ( meet S) is non empty;

      let F be sequence of M such that

       A17: F is Cauchy;

      consider S be non-empty closed SetSequence of M such that

       A18: S is non-ascending and

       A19: F is Cauchy implies S is pointwise_bounded & ( lim ( diameter S)) = 0 and

       A20: for i holds ex U be Subset of T st U = { (F . j) where j be Nat : j >= i } & (S . i) = ( Cl U) by Th9;

      set d = ( diameter S);



       A21: d is non-increasing by A17, A18, A19, Th2;

      ( meet S) is non empty by A16, A17, A18, A19;

      then

      consider x be object such that

       A22: x in ( meet S) by XBOOLE_0:def 1;



       A23: d is bounded_below by A17, A19, Th1;

      reconsider x as Point of M by A22;

      take x;

      let r;

      assume r > 0 ;

      then

      consider n be Nat such that

       A24: for m be Nat st n <= m holds |.((d . m) - 0 ).| < r by A17, A19, A23, A21, SEQ_2:def 7;

      take n;

      let m be Nat;

      assume n <= m;

      then

       A25: |.((d . m) - 0 ).| < r by A24;



       A26: (S . m) is bounded by A17, A19;



       A27: x in (S . m) by A22, KURATO_0: 3;



       A28: ( diameter (S . m)) = (d . m) by Def2;

      consider U be Subset of T such that

       A29: U = { (F . j) where j be Nat : j >= m } and

       A30: (S . m) = ( Cl U) by A20;



       A31: U c= ( Cl U) by PRE_TOPC: 18;

      (F . m) in U by A29;

      then

       A32: ( dist ((F . m),x)) <= ( diameter (S . m)) by A30, A31, A27, A26, TBSP_1:def 8;

      ( diameter (S . m)) >= 0 by A26, TBSP_1: 21;

      then (d . m) < r by A28, A25, ABSVALUE:def 1;

      hence thesis by A32, A28, XXREAL_0: 2;

    end;

    theorem :: COMPL_SP:11



     Th11: for T be non empty TopSpace holds for S be non-empty SetSequence of T st S is non-ascending holds for F be Subset-Family of T st F = ( rng S) holds F is centered

    proof

      let T be non empty TopSpace;

      let S be non-empty SetSequence of T such that

       A1: S is non-ascending;

      let F be Subset-Family of T such that

       A2: F = ( rng S);

       A3:

      now

        defpred P[ object, object] means $1 = (S . $2);

        let G be set such that

         A4: G <> {} and

         A5: G c= F and

         A6: G is finite;



         A7: for x be object st x in G holds ex y be object st y in NAT & P[x, y]

        proof

          let x be object;

          assume x in G;

          then ex y be object st y in ( dom S) & (S . y) = x by A2, A5, FUNCT_1:def 3;

          hence thesis;

        end;

        consider f be Function of G, NAT such that

         A8: for x be object st x in G holds P[x, (f . x)] from FUNCT_2:sch 1( A7);

        consider i be Nat such that

         A9: for j be Nat st j in ( rng f) holds j <= i by A6, STIRL2_1: 56;



         A10: i in NAT by ORDINAL1:def 12;

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

        then (S . i) <> {} by A10, FUNCT_1:def 9;

        then

        consider x be object such that

         A11: x in (S . i) by XBOOLE_0:def 1;



         A12: ( dom f) = G by FUNCT_2:def 1;

        now

          let Y be set;

          assume

           A13: Y in G;

          then

           A14: (f . Y) in ( rng f) by A12, FUNCT_1:def 3;

          reconsider fY = (f . Y) as Nat;



           A15: fY <= i by A9, A14;

          Y = (S . fY) by A8, A13;

          then (S . i) c= Y by A1, A15, PROB_1:def 4;

          hence x in Y by A11;

        end;

        hence ( meet G) <> {} by A4, SETFAM_1:def 1;

      end;

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

      then F <> {} by A2, RELAT_1: 42;

      hence thesis by A3, FINSET_1:def 3;

    end;

    theorem :: COMPL_SP:12



     Th12: for M be non empty MetrStruct holds for S be SetSequence of M holds for F be Subset-Family of ( TopSpaceMetr M) st F = ( rng S) holds (S is open implies F is open) & (S is closed implies F is closed)

    proof

      let M be non empty MetrStruct;

      let S be SetSequence of M;

      set T = ( TopSpaceMetr M);

      let F be Subset-Family of T such that

       A1: F = ( rng S);

      thus S is open implies F is open

      proof

        assume

         A2: S is open;

        let P be Subset of T;

        assume P in F;

        then

        consider x be object such that

         A3: x in ( dom S) and

         A4: (S . x) = P by A1, FUNCT_1:def 3;

        reconsider x as Nat by A3;

        (S . x) is open by A2;

        hence thesis by A4, Th6;

      end;

      assume

       A5: S is closed;

      let P be Subset of T;

      assume P in F;

      then

      consider x be object such that

       A6: x in ( dom S) and

       A7: (S . x) = P by A1, FUNCT_1:def 3;

      reconsider x as Nat by A6;

      (S . x) is closed by A5;

      hence thesis by A7, Th6;

    end;

    theorem :: COMPL_SP:13



     Th13: for T be non empty TopSpace holds for F be Subset-Family of T holds for S be SetSequence of T st ( rng S) c= F holds ex R be SetSequence of T st R is non-ascending & (F is centered implies R is non-empty) & (F is open implies R is open) & (F is closed implies R is closed) & for i holds (R . i) = ( meet { (S . j) where j be Element of NAT : j <= i })

    proof

      let T be non empty TopSpace;

      let F be Subset-Family of T;

      let S be SetSequence of T such that

       A1: ( rng S) c= F;



       A2: for i holds { (S . j) where j be Element of NAT : j <= i } c= F

      proof

        let i;

        let x be object;

        assume x in { (S . j) where j be Element of NAT : j <= i };

        then

        consider j be Element of NAT such that

         A3: x = (S . j) & j <= i;

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

        then x in ( rng S) by A3, FUNCT_1:def 3;

        hence thesis by A1;

      end;

      defpred P[ object, object] means for i st i = $1 holds $2 = ( meet { (S . j) where j be Element of NAT : j <= i });



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

      proof

        let x be object;

        assume x in NAT ;

        then

        reconsider i = x as Element of NAT ;

        set SS = { (S . j) where j be Element of NAT : j <= i };

        SS c= F by A2;

        then

        reconsider SS as Subset-Family of T by XBOOLE_1: 1;

        take ( meet SS);

        thus thesis;

      end;

      consider R be SetSequence of T such that

       A5: for x be object st x in NAT holds P[x, (R . x)] from FUNCT_2:sch 1( A4);

      take R;

      now

        let i be Nat;



         A6: i in NAT by ORDINAL1:def 12;

        set SS = { (S . j) where j be Element of NAT : j <= i };

        set S1 = { (S . j) where j be Element of NAT : j <= (i + 1) };



         A7: SS c= S1

        proof

          let x be object;

          assume x in SS;

          then

          consider j be Element of NAT such that

           A8: x = (S . j) and

           A9: j <= i;

          j <= (i + 1) by A9, NAT_1: 13;

          hence thesis by A8;

        end;



         A10: ( meet SS) = (R . i) by A5, A6;

        (S . 0 ) in SS;

        then ( meet S1) c= ( meet SS) by A7, SETFAM_1: 6;

        hence (R . (i + 1)) c= (R . i) by A5, A10;

      end;

      hence R is non-ascending by KURATO_0:def 3;



       A11: for i holds { (S . j) where j be Element of NAT : j <= i } is finite

      proof

        deffunc F( set) = (S . $1);

        let i;

        set SS = { (S . j) where j be Element of NAT : j <= i };



         A12: SS c= { F(j) where j be Element of NAT : j in (i + 1) }

        proof

          let x be object;

          assume x in SS;

          then

          consider j be Element of NAT such that

           A13: x = (S . j) and

           A14: j <= i;

          j < (i + 1) by A14, NAT_1: 13;

          then j in ( Segm (i + 1)) by NAT_1: 44;

          hence thesis by A13;

        end;



         A15: (i + 1) is finite;

        { F(j) where j be Element of NAT : j in (i + 1) } is finite from FRAENKEL:sch 21( A15);

        hence thesis by A12;

      end;

      thus F is centered implies R is non-empty

      proof

        assume

         A16: F is centered;

        now

          let x be object;

          assume x in ( dom R);

          then

          reconsider i = x as Element of NAT ;

          set SS = { (S . j) where j be Element of NAT : j <= i };



           A17: (S . 0 ) in SS;



           A18: SS c= F by A2;

          SS is finite by A11;

          then ( meet SS) <> {} by A16, A17, A18, FINSET_1:def 3;

          hence (R . x) is non empty by A5;

        end;

        hence thesis by FUNCT_1:def 9;

      end;

      thus F is open implies R is open

      proof

        assume

         A19: F is open;

        let i;

        set SS = { (S . j) where j be Element of NAT : j <= i };



         A20: SS c= F by A2;

        then

        reconsider SS as Subset-Family of T by XBOOLE_1: 1;

        SS is finite by A11;

        then

         A21: ( meet SS) is open by A19, A20, TOPS_2: 11, TOPS_2: 20;

        i in NAT by ORDINAL1:def 12;

        hence thesis by A5, A21;

      end;

      thus F is closed implies R is closed

      proof

        assume

         A22: F is closed;

        let i;

        set SS = { (S . j) where j be Element of NAT : j <= i };



         A23: i in NAT by ORDINAL1:def 12;



         A24: SS c= F by A2;

        then

        reconsider SS as Subset-Family of T by XBOOLE_1: 1;

        ( meet SS) is closed by A22, A24, TOPS_2: 12, TOPS_2: 22;

        hence thesis by A5, A23;

      end;

      let i;

      i in NAT by ORDINAL1:def 12;

      hence thesis by A5;

    end;

    theorem :: COMPL_SP:14

    for M be non empty MetrSpace holds M is complete iff for F be Subset-Family of ( TopSpaceMetr M) st F is closed & F is centered & for r be Real st r > 0 holds ex A be Subset of M st A in F & A is bounded & ( diameter A) < r holds ( meet F) is non empty

    proof

      let M be non empty MetrSpace;

      set T = ( TopSpaceMetr M);

      thus M is complete implies for F be Subset-Family of T st F is closed & F is centered & for r st r > 0 holds ex A be Subset of M st A in F & A is bounded & ( diameter A) < r holds ( meet F) is non empty

      proof

        reconsider NULL = 0 as Real;

        deffunc F( Nat) = (1 / (1 + $1));

        assume

         A1: M is complete;

        consider seq be Real_Sequence such that

         A2: for n be Nat holds (seq . n) = F(n) from SEQ_1:sch 1;

        set Ns = (NULL (#) seq);

        let F be Subset-Family of T such that

         A3: F is closed and

         A4: F is centered and

         A5: for r st r > 0 holds ex A be Subset of M st A in F & A is bounded & ( diameter A) < r;



         A6: for n be Nat holds (seq . n) = (1 / (n + 1)) by A2;

        then

         A7: Ns is convergent by SEQ_2: 7, SEQ_4: 31;

        defpred P[ object, object] means for i st i = $1 holds for A be Subset of M st A = $2 holds A in F & A is bounded & ( diameter A) < (1 / (i + 1));



         A8: for x be object st x in NAT holds ex y be object st y in ( bool the carrier of M) & P[x, y]

        proof

          let x be object;

          assume x in NAT ;

          then

          reconsider i = x as Nat;

          consider A be Subset of M such that

           A9: A in F and

           A10: A is bounded and

           A11: ( diameter A) < (1 / (i + 1)) by A5, XREAL_1: 139;

          take A;

          thus thesis by A9, A10, A11;

        end;

        consider f be SetSequence of M such that

         A12: for x be object st x in NAT holds P[x, (f . x)] from FUNCT_2:sch 1( A8);

        ( rng f) c= F

        proof

          let x be object;

          assume x in ( rng f);

          then

          consider y be object such that

           A13: y in ( dom f) and

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

          reconsider y as Element of NAT by A13;

          (f . y) in F by A12;

          hence thesis by A14;

        end;

        then

        consider R be SetSequence of T such that

         A15: R is non-ascending and

         A16: F is centered implies R is non-empty and F is open implies R is open and

         A17: F is closed implies R is closed and

         A18: for i holds (R . i) = ( meet { (f . j) where j be Element of NAT : j <= i }) by Th13;

        reconsider R9 = R as non-empty SetSequence of M by A4, A16;

        now

          let i;

          (f . 0 ) in { (f . j) where j be Element of NAT : j <= i };

          then ( meet { (f . j) where j be Element of NAT : j <= i }) c= (f . 0 ) by SETFAM_1: 3;

          then (R . i) c= (f . 0 ) by A18;

          hence (R9 . i) is bounded by A12, TBSP_1: 14;

        end;

        then

        reconsider R9 as non-empty pointwise_bounded SetSequence of M by Def1;

        set dR = ( diameter R9);

         A19:

        now

          let n be Nat;



           A20: n in NAT by ORDINAL1:def 12;

          set Sn = { (f . j) where j be Element of NAT : j <= n };



           A21: (f . n) in Sn by A20;

          (R . n) = ( meet Sn) by A18;

          then

           A22: (R . n) c= (f . n) by A21, SETFAM_1: 3;

          then ( diameter (R9 . n)) <= ( diameter (f . n)) by A12, TBSP_1: 24, A20;

          then

           A23: ( diameter (R9 . n)) <= F(n) by A12, XXREAL_0: 2, A20;

          (f . n) is bounded by A12, A20;

          then

           A24: 0 <= ( diameter (R9 . n)) by A22, TBSP_1: 14, TBSP_1: 21;



           A25: (Ns . n) = (NULL * (seq . n)) by SEQ_1: 9;

           F(n) = (seq . n) by A2;

          hence (Ns . n) <= (dR . n) & (dR . n) <= (seq . n) by A24, A23, A25, Def2;

        end;



         A26: ( lim seq) = 0 by A6, SEQ_4: 31;

        then

         A27: ( lim Ns) = (NULL * 0 ) by A6, SEQ_2: 8, SEQ_4: 31;



         A28: seq is convergent by A6, SEQ_4: 31;

        then

         A29: ( lim dR) = 0 by A26, A7, A27, A19, SEQ_2: 20;



         A30: R9 is closed by A3, A17, Th7;

        then ( meet R9) <> {} by A1, A15, A29, Th10;

        then

        consider x0 be object such that

         A31: x0 in ( meet R9) by XBOOLE_0:def 1;

        reconsider x0 as Point of M by A31;



         A32: dR is convergent by A28, A26, A7, A27, A19, SEQ_2: 19;

         A33:

        now

          let y;

          assume

           A34: y in F;

          then

          reconsider Y = y as Subset of T;

          defpred P9[ object, object] means for i st i = $1 holds $2 = ((R . i) /\ Y);



           A35: for x be object st x in NAT holds ex z be object st z in ( bool the carrier of M) & P9[x, z]

          proof

            let x be object;

            assume x in NAT ;

            then

            reconsider i = x as Nat;

            take ((R . i) /\ Y);

            thus thesis;

          end;

          consider f9 be SetSequence of M such that

           A36: for x be object st x in NAT holds P9[x, (f9 . x)] from FUNCT_2:sch 1( A35);

           A37:

          now

            deffunc F( object) = (f . $1);

            let x be object;

            assume x in ( dom f9);

            then

            reconsider i = x as Element of NAT ;

            set SS = { (f . j) where j be Element of NAT : j <= i };



             A38: (f . i) in SS;



             A39: SS c= { F(j) where j be Element of NAT : j in (i + 1) }

            proof

              let x be object;

              assume x in SS;

              then

              consider j be Element of NAT such that

               A40: x = (f . j) and

               A41: j <= i;

              j < (i + 1) by A41, NAT_1: 13;

              then j in ( Segm (i + 1)) by NAT_1: 44;

              hence thesis by A40;

            end;



             A42: ( {Y} \/ SS) c= F

            proof

              let z be object such that

               A43: z in ( {Y} \/ SS);

              per cases by A43, XBOOLE_0:def 3;

                suppose z in {Y};

                hence thesis by A34, TARSKI:def 1;

              end;

                suppose z in SS;

                then ex j be Element of NAT st z = (f . j) & j <= i;

                hence thesis by A12;

              end;

            end;



             A44: (i + 1) is finite;

            { F(j) where j be Element of NAT : j in (i + 1) } is finite from FRAENKEL:sch 21( A44);

            then ( meet ( {Y} \/ SS)) <> {} by A4, A42, A39, FINSET_1:def 3;

            then (( meet {Y}) /\ ( meet SS)) <> {} by A38, SETFAM_1: 9;

            then (Y /\ ( meet SS)) <> {} by SETFAM_1: 10;

            then (Y /\ (R . i)) <> {} by A18;

            hence (f9 . x) is non empty by A36;

          end;

           A45:

          now

            let i;

            reconsider Ri = (R . i) as Subset of T;

            i in NAT by ORDINAL1:def 12;

            then

             A46: (f9 . i) = (Ri /\ Y) by A36;

            (R9 . i) is closed by A30;

            then

             A47: Ri is closed by Th6;

            Y is closed by A3, A34;

            hence (f9 . i) is closed by A47, A46, Th6;

          end;

          now

            let i;

            i in NAT by ORDINAL1:def 12;

            then

             A48: (f9 . i) = ((R9 . i) /\ Y) by A36;

            (R9 . i) is bounded by Def1;

            hence (f9 . i) is bounded by A48, TBSP_1: 14, XBOOLE_1: 17;

          end;

          then

          reconsider f9 as non-empty pointwise_bounded closed SetSequence of M by A37, A45, Def1, Def8, FUNCT_1:def 9;



           A49: (f9 . 0 ) = ((R . 0 ) /\ Y) by A36;

          set df = ( diameter f9);

          now

            reconsider Y9 = Y as Subset of M;

            let n be Nat;



             A50: (Ns . n) = (NULL * (seq . n)) by SEQ_1: 9;

            n in NAT by ORDINAL1:def 12;

            then

             A51: ((R . n) /\ Y9) = (f9 . n) by A36;



             A52: (R9 . n) is bounded by Def1;

            then ( diameter (f9 . n)) <= ( diameter (R9 . n)) by A51, TBSP_1: 24, XBOOLE_1: 17;

            then

             A53: ( diameter (f9 . n)) <= (dR . n) by Def2;

            ((R . n) /\ Y) c= (R . n) by XBOOLE_1: 17;

            then 0 <= ( diameter (f9 . n)) by A52, A51, TBSP_1: 14, TBSP_1: 21;

            hence (Ns . n) <= (df . n) & (df . n) <= (dR . n) by A53, A50, Def2;

          end;

          then

           A54: ( lim df) = 0 by A7, A27, A32, A29, SEQ_2: 20;

          now

            let i be Nat;

            i in NAT by ORDINAL1:def 12;

            then

             A55: (f9 . i) = ((R . i) /\ Y) by A36;



             A56: (R . (i + 1)) c= (R . i) by A15, KURATO_0:def 3;

            (f9 . (i + 1)) = ((R . (i + 1)) /\ Y) by A36;

            hence (f9 . (i + 1)) c= (f9 . i) by A55, A56, XBOOLE_1: 26;

          end;

          then f9 is non-ascending by KURATO_0:def 3;

          then ( meet f9) <> {} by A1, A54, Th10;

          then

          consider z be object such that

           A57: z in ( meet f9) by XBOOLE_0:def 1;

          reconsider z as Point of M by A57;



           A58: x0 = z

          proof

            assume x0 <> z;

            then ( dist (x0,z)) <> 0 by METRIC_1: 2;

            then ( dist (x0,z)) > 0 by METRIC_1: 5;

            then

            consider i be Nat such that

             A59: for j be Nat st i <= j holds |.((dR . j) - 0 ).| < ( dist (x0,z)) by A32, A29, SEQ_2:def 7;



             A60: i in NAT by ORDINAL1:def 12;



             A61: (f9 . i) = ((R . i) /\ Y) by A36, A60;

            z in (f9 . i) by A57, KURATO_0: 3;

            then

             A62: z in (R . i) by A61, XBOOLE_0:def 4;



             A63: (R9 . i) is bounded by Def1;

            then

             A64: 0 <= ( diameter (R9 . i)) by TBSP_1: 21;

            x0 in (R . i) by A31, KURATO_0: 3;

            then ( dist (x0,z)) <= ( diameter (R9 . i)) by A62, A63, TBSP_1:def 8;

            then

             A65: |.( diameter (R9 . i)).| >= ( dist (x0,z)) by A64, ABSVALUE:def 1;

             |.((dR . i) - 0 ).| < ( dist (x0,z)) by A59;

            hence thesis by A65, Def2;

          end;

          z in (f9 . 0 ) by A57, KURATO_0: 3;

          hence x0 in y by A58, A49, XBOOLE_0:def 4;

        end;

        F <> {} by A4, FINSET_1:def 3;

        hence thesis by A33, SETFAM_1:def 1;

      end;

      assume

       A66: for F be Subset-Family of T st F is closed & F is centered & for r st r > 0 holds ex A be Subset of M st A in F & A is bounded & ( diameter A) < r holds ( meet F) is non empty;

      now

        let S be non-empty pointwise_bounded closed SetSequence of M such that

         A67: S is non-ascending and

         A68: ( lim ( diameter S)) = 0 ;

        reconsider RS = ( rng S) as Subset-Family of T;

         A69:

        now

          set d = ( diameter S);



           A70: ( dom S) = NAT by FUNCT_2:def 1;



           A71: d is bounded_below by Th1;



           A72: d is non-increasing by A67, Th2;

          let r;

          assume r > 0 ;

          then

          consider n be Nat such that

           A73: for m be Nat st n <= m holds |.((d . m) - 0 ).| < r by A68, A71, A72, SEQ_2:def 7;

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

          take Sn = (S . nn);



           A74: (d . n) = ( diameter Sn) by Def2;

          Sn is bounded by Def1;

          then

           A75: ( diameter Sn) >= 0 by TBSP_1: 21;

           |.((d . n) - 0 ).| < r by A73;

          hence Sn in RS & Sn is bounded & ( diameter Sn) < r by A74, A75, A70, Def1, ABSVALUE:def 1, FUNCT_1:def 3;

        end;

        RS is closed by Th12;

        then ( meet RS) is non empty by A66, A67, A69, Th11;

        then

        consider x be object such that

         A76: x in ( meet RS) by XBOOLE_0:def 1;

        now

          let i be Nat;



           A77: i in NAT by ORDINAL1:def 12;

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

          then (S . i) in RS by FUNCT_1:def 3, A77;

          hence x in (S . i) by A76, SETFAM_1:def 1;

        end;

        hence ( meet S) is non empty by KURATO_0: 3;

      end;

      hence thesis by Th10;

    end;

    theorem :: COMPL_SP:15



     Th15: for M be non empty MetrSpace, A be non empty Subset of M holds for B be Subset of M, B9 be Subset of (M | A) st B = B9 holds B9 is bounded iff B is bounded

    proof

      let M be non empty MetrSpace, A be non empty Subset of M;

      let B be Subset of M, B9 be Subset of (M | A) such that

       A1: B = B9;

      thus B9 is bounded implies B is bounded by A1, HAUSDORF: 17;

      assume

       A2: B is bounded;

      per cases ;

        suppose B9 = ( {} (M | A));

        hence thesis;

      end;

        suppose B9 <> ( {} (M | A));

        then

        consider p be object such that

         A3: p in B9 by XBOOLE_0:def 1;

        reconsider p as Point of (M | A) by A3;

         A4:

        now

          let q be Point of (M | A) such that

           A5: q in B9;

          reconsider p9 = p, q9 = q as Point of M by TOPMETR: 8;



           A6: ( dist (p,q)) = ( dist (p9,q9)) by TOPMETR:def 1;



           A7: (( diameter B) + 0 ) <= (( diameter B) + 1) by XREAL_1: 8;

          ( dist (p9,q9)) <= ( diameter B) by A1, A2, A3, A5, TBSP_1:def 8;

          hence ( dist (p,q)) <= (( diameter B) + 1) by A6, A7, XXREAL_0: 2;

        end;

        ( 0 + 0 ) < (( diameter B) + 1) by A2, TBSP_1: 21, XREAL_1: 8;

        hence thesis by A4, TBSP_1: 10;

      end;

    end;

    theorem :: COMPL_SP:16



     Th16: for M be non empty MetrSpace, A be non empty Subset of M holds for B be Subset of M, B9 be Subset of (M | A) st B = B9 & B is bounded holds ( diameter B9) <= ( diameter B)

    proof

      let M be non empty MetrSpace, A be non empty Subset of M;

      let B be Subset of M, B9 be Subset of (M | A) such that

       A1: B = B9 and

       A2: B is bounded;



       A3: B9 is bounded by A1, A2, Th15;

      per cases ;

        suppose

         A4: B9 = ( {} (M | A));

        then ( diameter B9) = 0 by TBSP_1:def 8;

        hence thesis by A1, A4, TBSP_1:def 8;

      end;

        suppose

         A5: B9 <> ( {} (M | A));

        now

          let x,y be Point of (M | A) such that

           A6: x in B9 and

           A7: y in B9;

          reconsider x9 = x, y9 = y as Point of M by TOPMETR: 8;

          ( dist (x,y)) = ( dist (x9,y9)) by TOPMETR:def 1;

          hence ( dist (x,y)) <= ( diameter B) by A1, A2, A6, A7, TBSP_1:def 8;

        end;

        hence thesis by A3, A5, TBSP_1:def 8;

      end;

    end;

    theorem :: COMPL_SP:17



     Th17: for M be non empty MetrSpace, A be non empty Subset of M holds for S be sequence of (M | A) holds S is sequence of M

    proof

      let M be non empty MetrSpace, A be non empty Subset of M;

      let S be sequence of (M | A);

      A c= the carrier of M;

      then the carrier of (M | A) c= the carrier of M by TOPMETR:def 2;

      hence thesis by FUNCT_2: 7;

    end;

    theorem :: COMPL_SP:18



     Th18: for M be non empty MetrSpace, A be non empty Subset of M holds for S be sequence of (M | A), S9 be sequence of M st S = S9 holds S9 is Cauchy iff S is Cauchy

    proof

      let M be non empty MetrSpace, A be non empty Subset of M;

      let S be sequence of (M | A), S9 be sequence of M such that

       A1: S = S9;

      thus S9 is Cauchy implies S is Cauchy

      proof

        assume

         A2: S9 is Cauchy;

        let r;

        assume r > 0 ;

        then

        consider p be Nat such that

         A3: for n,m be Nat st p <= n & p <= m holds ( dist ((S9 . n),(S9 . m))) < r by A2;

        take p;

        let n,m be Nat such that

         A4: p <= n and

         A5: p <= m;

        ( dist ((S . n),(S . m))) = ( dist ((S9 . n),(S9 . m))) by A1, TOPMETR:def 1;

        hence thesis by A3, A4, A5;

      end;

      assume

       A6: S is Cauchy;

      let r;

      assume r > 0 ;

      then

      consider p be Nat such that

       A7: for n,m be Nat st p <= n & p <= m holds ( dist ((S . n),(S . m))) < r by A6;

      take p;

      let n,m be Nat such that

       A8: p <= n and

       A9: p <= m;

      ( dist ((S . n),(S . m))) = ( dist ((S9 . n),(S9 . m))) by A1, TOPMETR:def 1;

      hence thesis by A7, A8, A9;

    end;

    theorem :: COMPL_SP:19

    for M be non empty MetrSpace st M is complete holds for A be non empty Subset of M, A9 be Subset of ( TopSpaceMetr M) st A = A9 holds (M | A) is complete iff A9 is closed

    proof

      let M be non empty MetrSpace such that

       A1: M is complete;

      set T = ( TopSpaceMetr M);

      let A be non empty Subset of M, A9 be Subset of ( TopSpaceMetr M) such that

       A2: A = A9;

      set MA = (M | A);

      set TA = ( TopSpaceMetr MA);

      thus MA is complete implies A9 is closed

      proof

        assume

         A3: MA is complete;



         A4: ( Cl A9) c= A9

        proof

          let p be object such that

           A5: p in ( Cl A9);

          reconsider p as Point of M by A5;

          defpred P[ object, object] means for i st i = $1 holds $2 = (A /\ ( cl_Ball (p,(1 / (i + 1)))));



           A6: for x be object st x in NAT holds ex y be object st y in ( bool the carrier of MA) & P[x, y]

          proof

            let x be object;

            assume x in NAT ;

            then

            reconsider i = x as Nat;

            take (A /\ ( cl_Ball (p,(1 / (i + 1)))));

            (A /\ ( cl_Ball (p,(1 / (i + 1))))) c= A by XBOOLE_1: 17;

            then (A /\ ( cl_Ball (p,(1 / (i + 1))))) c= the carrier of MA by TOPMETR:def 2;

            hence thesis;

          end;

          consider f be SetSequence of MA such that

           A7: for x be object st x in NAT holds P[x, (f . x)] from FUNCT_2:sch 1( A6);

           A8:

          now

            let x be object;

            assume x in ( dom f);

            then

            reconsider i = x as Element of NAT ;

            reconsider B = ( Ball (p,(1 / (i + 1)))) as Subset of T;

            ( Ball (p,(1 / (i + 1)))) in ( Family_open_set M) by PCOMPS_1: 29;

            then

             A9: B is open by PRE_TOPC:def 2;

            p in B by TBSP_1: 11, XREAL_1: 139;

            then B meets A9 by A5, A9, PRE_TOPC: 24;

            then

            consider y be object such that

             A10: y in B and

             A11: y in A9 by XBOOLE_0: 3;

            reconsider y as Point of M by A10;

            ( dist (p,y)) < (1 / (i + 1)) by A10, METRIC_1: 11;

            then y in ( cl_Ball (p,(1 / (i + 1)))) by METRIC_1: 12;

            then y in (A /\ ( cl_Ball (p,(1 / (i + 1))))) by A2, A11, XBOOLE_0:def 4;

            hence (f . x) is non empty by A7;

          end;

           A12:

          now

            let i;

            reconsider cB = ( cl_Ball (p,(1 / (i + 1)))) as Subset of T;

            reconsider fi = (f . i) as Subset of TA;



             A13: i in NAT by ORDINAL1:def 12;

            (( [#] M) \ cB) in ( Family_open_set M) by NAGATA_1: 14;

            then (cB ` ) is open by PRE_TOPC:def 2;

            then

             A14: cB is closed by TOPS_1: 3;



             A15: TA = (T | A9) by A2, HAUSDORF: 16;

            then ( [#] (T | A9)) = A by TOPMETR:def 2;

            then fi = (cB /\ ( [#] (T | A9))) by A7, A13;

            then fi is closed by A14, A15, PRE_TOPC: 13;

            hence (f . i) is closed by Th6;

          end;

          now

            let i;

            set ACL = (A /\ ( cl_Ball (p,(1 / (i + 1)))));

            ( cl_Ball (p,(1 / (i + 1)))) is bounded by TOPREAL6: 59;

            then

             A16: ACL is bounded by TBSP_1: 14, XBOOLE_1: 17;

            i in NAT by ORDINAL1:def 12;

            then (f . i) = ACL by A7;

            hence (f . i) is bounded by A16, Th15;

          end;

          then

          reconsider f as non-empty pointwise_bounded closed SetSequence of MA by A8, A12, Def1, Def8, FUNCT_1:def 9;

          set df = ( diameter f);

          reconsider NULL = 0 , TWO = 2 as Real;

          deffunc F( Nat) = (1 / (1 + $1));

          consider seq be Real_Sequence such that

           A17: for n be Nat holds (seq . n) = F(n) from SEQ_1:sch 1;

          now

            let i be Nat;

            set i1 = (i + 1);

            ( cl_Ball (p,(1 / (i1 + 1)))) c= ( cl_Ball (p,(1 / i1)))

            proof

              let x be object such that

               A18: x in ( cl_Ball (p,(1 / (i1 + 1))));

              reconsider q = x as Point of M by A18;

              i1 < (i1 + 1) by NAT_1: 13;

              then

               A19: (1 / (i1 + 1)) < (1 / i1) by XREAL_1: 76;

              ( dist (p,q)) <= (1 / (i1 + 1)) by A18, METRIC_1: 12;

              then ( dist (p,q)) <= (1 / i1) by A19, XXREAL_0: 2;

              hence thesis by METRIC_1: 12;

            end;

            then

             A20: (A /\ ( cl_Ball (p,(1 / (i1 + 1))))) c= (A /\ ( cl_Ball (p,(1 / i1)))) by XBOOLE_1: 26;

            i in NAT by ORDINAL1:def 12;

            then (f . i) = (A /\ ( cl_Ball (p,(1 / i1)))) by A7;

            hence (f . (i + 1)) c= (f . i) by A7, A20;

          end;

          then

           A21: f is non-ascending by KURATO_0:def 3;

          set Ts = (TWO (#) seq);

          set Ns = (NULL (#) seq);



           A22: for n be Nat holds (seq . n) = (1 / (n + 1)) by A17;

          then

           A23: Ns is convergent by SEQ_2: 7, SEQ_4: 31;

           A24:

          now

            let n be Nat;

            set cB = ( cl_Ball (p,(1 / (n + 1))));



             A25: (Ns . n) = (NULL * (seq . n)) by SEQ_1: 9;



             A26: (Ts . n) = (TWO * (seq . n)) by SEQ_1: 9;



             A27: cB is bounded by TOPREAL6: 59;

            then

             A28: (A /\ cB) is bounded by TBSP_1: 14, XBOOLE_1: 17;



             A29: ( diameter (A /\ cB)) <= ( diameter cB) by A27, TBSP_1: 24, XBOOLE_1: 17;

            ( diameter cB) <= (2 * F(n)) by Th5;

            then

             A30: ( diameter (A /\ cB)) <= (2 * F(n)) by A29, XXREAL_0: 2;

            n in NAT by ORDINAL1:def 12;

            then

             A31: (f . n) = (A /\ cB) by A7;

            then (f . n) is bounded by A28, Th15;

            then

             A32: 0 <= ( diameter (f . n)) by TBSP_1: 21;

            ( diameter (f . n)) <= ( diameter (A /\ cB)) by A28, A31, Th16;

            then

             A33: ( diameter (f . n)) <= (2 * F(n)) by A30, XXREAL_0: 2;

             F(n) = (seq . n) by A17;

            hence (Ns . n) <= (df . n) & (df . n) <= (Ts . n) by A32, A33, A25, A26, Def2;

          end;



           A34: Ts is convergent by A22, SEQ_2: 7, SEQ_4: 31;



           A35: ( lim seq) = 0 by A22, SEQ_4: 31;

          then

           A36: ( lim Ts) = (TWO * 0 ) by A22, SEQ_2: 8, SEQ_4: 31;

          ( lim Ns) = (NULL * 0 ) by A22, A35, SEQ_2: 8, SEQ_4: 31;

          then ( lim df) = 0 by A23, A34, A36, A24, SEQ_2: 20;

          then ( meet f) is non empty by A3, A21, Th10;

          then

          consider q be object such that

           A37: q in ( meet f) by XBOOLE_0:def 1;

          reconsider q as Point of M by A37, TOPMETR: 8;



           A38: seq is convergent by A22, SEQ_4: 31;

          p = q

          proof

            assume p <> q;

            then ( dist (p,q)) <> 0 by METRIC_1: 2;

            then ( dist (p,q)) > 0 by METRIC_1: 5;

            then

            consider n be Nat such that

             A39: for m be Nat st n <= m holds |.((seq . m) - 0 ).| < ( dist (p,q)) by A38, A35, SEQ_2:def 7;

            set cB = ( cl_Ball (p,(1 / (n + 1))));



             A40: q in (f . n) by A37, KURATO_0: 3;

            n in NAT by ORDINAL1:def 12;

            then (f . n) = (A /\ cB) by A7;

            then q in cB by A40, XBOOLE_0:def 4;

            then

             A41: ( dist (p,q)) <= F(n) by METRIC_1: 12;

            (seq . n) = F(n) by A17;

            then |.((seq . n) - 0 ).| = F(n) by ABSVALUE:def 1;

            hence thesis by A39, A41;

          end;

          then

           A42: p in (f . 0 ) by A37, KURATO_0: 3;

          (f . 0 ) = (A /\ ( cl_Ball (p,(1 / ( 0 + 1))))) by A7;

          hence thesis by A2, A42, XBOOLE_0:def 4;

        end;

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

        hence thesis by A4, XBOOLE_0:def 10;

      end;

      assume

       A43: A9 is closed;

      let S be sequence of MA such that

       A44: S is Cauchy;

      reconsider S9 = S as sequence of M by Th17;

      S9 is Cauchy by A44, Th18;

      then

       A45: S9 is convergent by A1;

       A46:

      now

        let n be Nat;

        (S . n) in the carrier of (M | A);

        hence (S9 . n) in A9 by A2, TOPMETR:def 2;

      end;

      the carrier of (M | A) = A9 by A2, TOPMETR:def 2;

      then

      reconsider limS = ( lim S9) as Point of (M | A) by A43, A45, A46, TOPMETR3: 1;

      take limS;

      let r;

      assume r > 0 ;

      then

      consider n be Nat such that

       A47: for m be Nat st m >= n holds ( dist ((S9 . m),( lim S9))) < r by A45, TBSP_1:def 3;

      take n;

      let m be Nat such that

       A48: m >= n;

      ( dist ((S . m),limS)) = ( dist ((S9 . m),( lim S9))) by TOPMETR:def 1;

      hence thesis by A47, A48;

    end;

    begin

    definition

      let T be TopStruct;

      :: COMPL_SP:def9

      attr T is countably_compact means for F be Subset-Family of T st F is Cover of T & F is open & F is countable holds ex G be Subset-Family of T st G c= F & G is Cover of T & G is finite;

    end

    theorem :: COMPL_SP:20

    for T be TopStruct st T is compact holds T is countably_compact;

    theorem :: COMPL_SP:21



     Th21: for T be non empty TopSpace holds T is countably_compact iff for F be Subset-Family of T st F is centered & F is closed & F is countable holds ( meet F) <> {}

    proof

      let T be non empty TopSpace;

      thus T is countably_compact implies for F be Subset-Family of T st F is centered & F is closed & F is countable holds ( meet F) <> {}

      proof

        assume

         A1: T is countably_compact;

        let F be Subset-Family of T such that

         A2: F is centered and

         A3: F is closed and

         A4: F is countable;

        assume

         A5: ( meet F) = {} ;

        F <> {} by A2, FINSET_1:def 3;



        then ( union ( COMPLEMENT F)) = (( meet F) ` ) by TOPS_2: 7

        .= ( [#] T) by A5;

        then

         A6: ( COMPLEMENT F) is Cover of T by SETFAM_1: 45;



         A7: ( COMPLEMENT F) is countable by A4, TOPGEN_4: 1;

        ( COMPLEMENT F) is open by A3, TOPS_2: 9;

        then

        consider G9 be Subset-Family of T such that

         A8: G9 c= ( COMPLEMENT F) and

         A9: G9 is Cover of T and

         A10: G9 is finite by A1, A6, A7;



         A11: ( COMPLEMENT G9) is finite by A10, TOPS_2: 8;



         A12: ( COMPLEMENT G9) c= F

        proof

          let x be object such that

           A13: x in ( COMPLEMENT G9);

          reconsider x9 = x as Subset of T by A13;

          (x9 ` ) in G9 by A13, SETFAM_1:def 7;

          then ((x9 ` ) ` ) in F by A8, SETFAM_1:def 7;

          hence thesis;

        end;

        G9 <> {} by A9, TOPS_2: 3;

        then

         A14: ( COMPLEMENT G9) <> {} by TOPS_2: 5;

        ( meet ( COMPLEMENT G9)) = (( union G9) ` ) by A9, TOPS_2: 3, TOPS_2: 6

        .= (( [#] T) \ ( [#] T)) by A9, SETFAM_1: 45

        .= {} by XBOOLE_1: 37;

        hence contradiction by A2, A12, A14, A11, FINSET_1:def 3;

      end;

      assume

       A15: for F be Subset-Family of T st F is centered & F is closed & F is countable holds ( meet F) <> {} ;

      let F be Subset-Family of T such that

       A16: F is Cover of T and

       A17: F is open and

       A18: F is countable;



       A19: ( COMPLEMENT F) is countable by A18, TOPGEN_4: 1;

      F <> {} by A16, TOPS_2: 3;

      then

       A20: ( COMPLEMENT F) <> {} by TOPS_2: 5;



       A21: ( COMPLEMENT F) is closed by A17, TOPS_2: 10;

      ( meet ( COMPLEMENT F)) = (( union F) ` ) by A16, TOPS_2: 3, TOPS_2: 6

      .= (( [#] T) \ ( [#] T)) by A16, SETFAM_1: 45

      .= {} by XBOOLE_1: 37;

      then not ( COMPLEMENT F) is centered by A15, A19, A21;

      then

      consider G9 be set such that

       A22: G9 <> {} and

       A23: G9 c= ( COMPLEMENT F) and

       A24: G9 is finite and

       A25: ( meet G9) = {} by A20, FINSET_1:def 3;

      reconsider G9 as Subset-Family of T by A23, XBOOLE_1: 1;

      take F9 = ( COMPLEMENT G9);

      thus F9 c= F

      proof

        let x be object such that

         A26: x in F9;

        reconsider x9 = x as Subset of T by A26;

        (x9 ` ) in G9 by A26, SETFAM_1:def 7;

        then ((x9 ` ) ` ) in F by A23, SETFAM_1:def 7;

        hence thesis;

      end;

      ( union F9) = (( meet G9) ` ) by A22, TOPS_2: 7

      .= ( [#] T) by A25;

      hence thesis by A24, SETFAM_1: 45, TOPS_2: 8;

    end;

    theorem :: COMPL_SP:22



     Th22: for T be non empty TopSpace holds T is countably_compact iff for S be non-empty closed SetSequence of T st S is non-ascending holds ( meet S) <> {}

    proof

      let T be non empty TopSpace;

      thus T is countably_compact implies for S be non-empty closed SetSequence of T st S is non-ascending holds ( meet S) <> {}

      proof

        assume

         A1: T is countably_compact;

        let S be non-empty closed SetSequence of T such that

         A2: S is non-ascending;

        reconsider rngS = ( rng S) as Subset-Family of T;

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

        then

         A3: rngS is countable by CARD_3: 93;

        now

          let D be Subset of T;

          assume D in rngS;

          then ex x be object st x in ( dom S) & (S . x) = D by FUNCT_1:def 3;

          hence D is closed by Def6;

        end;

        then

         A4: rngS is closed;

        rngS is centered by A2, Th11;

        then ( meet rngS) <> {} by A1, A3, A4, Th21;

        then

        consider x be object such that

         A5: x in ( meet rngS) by XBOOLE_0:def 1;

        now

          let n be Nat;



           A6: n in NAT by ORDINAL1:def 12;

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

          then (S . n) in rngS by FUNCT_1:def 3, A6;

          hence x in (S . n) by A5, SETFAM_1:def 1;

        end;

        hence thesis by KURATO_0: 3;

      end;

      assume

       A7: for S be non-empty closed SetSequence of T st S is non-ascending holds ( meet S) <> {} ;

      now

        let F be Subset-Family of T such that

         A8: F is centered and

         A9: F is closed and

         A10: F is countable;



         A11: ( card F) c= omega by A10, CARD_3:def 14;

        now

          per cases by A11, CARD_1: 3;

            suppose ( card F) = omega ;

            then ( NAT ,F) are_equipotent by CARD_1: 5, CARD_1: 47;

            then

            consider s be Function such that s is one-to-one and

             A12: ( dom s) = NAT and

             A13: ( rng s) = F by WELLORD2:def 4;

            reconsider s as SetSequence of T by A12, A13, FUNCT_2: 2;

            consider R be SetSequence of T such that

             A14: R is non-ascending and

             A15: F is centered implies R is non-empty and F is open implies R is open and

             A16: F is closed implies R is closed and

             A17: for i holds (R . i) = ( meet { (s . j) where j be Element of NAT : j <= i }) by A13, Th13;

            ( meet R) <> {} by A7, A8, A9, A14, A15, A16;

            then

            consider x be object such that

             A18: x in ( meet R) by XBOOLE_0:def 1;

             A19:

            now

              let y;

              assume y in F;

              then

              consider z be object such that

               A20: z in ( dom s) and

               A21: (s . z) = y by A13, FUNCT_1:def 3;

              reconsider z as Element of NAT by A20;



               A22: (s . z) in { (s . j) where j be Element of NAT : j <= z };



               A23: x in (R . z) by A18, KURATO_0: 3;

              (R . z) = ( meet { (s . j) where j be Element of NAT : j <= z }) by A17;

              then (R . z) c= (s . z) by A22, SETFAM_1: 3;

              hence x in y by A21, A23;

            end;

            F is non empty by A12, A13, RELAT_1: 42;

            hence ( meet F) is non empty by A19, SETFAM_1:def 1;

          end;

            suppose

             A24: ( card F) in omega ;

            F is finite by A24;

            hence ( meet F) is non empty by A8, FINSET_1:def 3;

          end;

        end;

        hence ( meet F) <> {} ;

      end;

      hence thesis by Th21;

    end;

    theorem :: COMPL_SP:23



     Th23: for T be non empty TopSpace holds for F be Subset-Family of T holds for S be SetSequence of T st ( rng S) c= F & S is non-empty holds ex R be non-empty closed SetSequence of T st R is non-ascending & (F is locally_finite & S is one-to-one implies ( meet R) = {} ) & for i holds ex Si be Subset-Family of T st (R . i) = ( Cl ( union Si)) & Si = { (S . j) where j be Element of NAT : j >= i }

    proof

      let T be non empty TopSpace;

      let F be Subset-Family of T;

      let S be SetSequence of T such that

       A1: ( rng S) c= F and

       A2: S is non-empty;

      defpred r[ object, object] means for i st i = $1 holds ex SS be Subset-Family of T st SS c= F & SS = { (S . j) where j be Element of NAT : j >= i } & $2 = ( Cl ( union SS));



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

      proof

        let x be object;

        assume x in NAT ;

        then

        reconsider x9 = x as Nat;

        set SS = { (S . j) where j be Element of NAT : j >= x9 };

        SS c= ( bool the carrier of T)

        proof

          let y be object;

          assume y in SS;

          then ex j be Element of NAT st (S . j) = y & j >= x9;

          hence thesis;

        end;

        then

        reconsider SS as Subset-Family of T;

        take ( Cl ( union SS));

        SS c= F

        proof

          let y be object;

          assume y in SS;

          then

          consider j be Element of NAT such that

           A4: (S . j) = y & j >= x9;

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

          then y in ( rng S) by A4, FUNCT_1:def 3;

          hence thesis by A1;

        end;

        hence thesis;

      end;

      consider R be SetSequence of T such that

       A5: for x be object st x in NAT holds r[x, (R . x)] from FUNCT_2:sch 1( A3);

       A6:

      now

        let n be object;

        assume n in ( dom R);

        then

        reconsider n9 = n as Element of NAT ;



         A7: (S . n9) c= ( Cl (S . n9)) by PRE_TOPC: 18;

        consider SS be Subset-Family of T such that SS c= F and

         A8: SS = { (S . j) where j be Element of NAT : j >= n9 } and

         A9: (R . n9) = ( Cl ( union SS)) by A5;

        (S . n9) in SS by A8;

        then

         A10: ( Cl (S . n9)) c= ( Cl ( union SS)) by PRE_TOPC: 19, ZFMISC_1: 74;

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

        hence (R . n) is non empty by A2, A9, A7, A10, FUNCT_1:def 9;

      end;

      now

        let n;

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

        ex SS be Subset-Family of T st SS c= F & SS = { (S . j) where j be Element of NAT : j >= n9 } & (R . n9) = ( Cl ( union SS)) by A5;

        hence (R . n) is closed;

      end;

      then

      reconsider R as non-empty closed SetSequence of T by A6, Def6, FUNCT_1:def 9;

      take R;

      now

        let n be Nat;



         A11: n in NAT by ORDINAL1:def 12;

        consider Sn be Subset-Family of T such that Sn c= F and

         A12: Sn = { (S . j) where j be Element of NAT : j >= n } and

         A13: (R . n) = ( Cl ( union Sn)) by A5, A11;

        consider Sn1 be Subset-Family of T such that Sn1 c= F and

         A14: Sn1 = { (S . j) where j be Element of NAT : j >= (n + 1) } and

         A15: (R . (n + 1)) = ( Cl ( union Sn1)) by A5;

        Sn1 c= Sn

        proof

          let y be object;

          assume y in Sn1;

          then

          consider j be Element of NAT such that

           A16: y = (S . j) and

           A17: j >= (n + 1) by A14;

          j >= n by A17, NAT_1: 13;

          hence thesis by A12, A16;

        end;

        then ( union Sn1) c= ( union Sn) by ZFMISC_1: 77;

        hence (R . (n + 1)) c= (R . n) by A13, A15, PRE_TOPC: 19;

      end;

      hence R is non-ascending by KURATO_0:def 3;

      thus F is locally_finite & S is one-to-one implies ( meet R) = {}

      proof



         A18: ( dom S) = NAT by FUNCT_2:def 1;

        then

        reconsider rngS = ( rng S) as non empty Subset-Family of T by RELAT_1: 42;

        reconsider Sp = S as sequence of rngS by A18, FUNCT_2: 1;

        assume that

         A19: F is locally_finite and

         A20: S is one-to-one;

        reconsider S9 = (Sp " ) as Function;

        reconsider S9 as Function of rngS, NAT by A20, FUNCT_2: 25;

        deffunc s9( Element of rngS) = (S9 . $1);

        assume ( meet R) <> {} ;

        then

        consider x be object such that

         A21: x in ( meet R) by XBOOLE_0:def 1;

        reconsider x as Point of T by A21;

        ( rng S) is locally_finite by A1, A19, PCOMPS_1: 9;

        then

        consider W be Subset of T such that

         A22: x in W and

         A23: W is open and

         A24: { V where V be Subset of T : V in rngS & V meets W } is finite;

        set X = { V where V be Subset of T : V in rngS & V meets W };

        set Y = { s9(z) where z be Element of rngS : z in X };



         A25: Y is finite from FRAENKEL:sch 21( A24);

        Y c= NAT

        proof

          let y be object;

          assume y in Y;

          then ex z be Element of rngS st y = s9(z) & z in X;

          hence thesis;

        end;

        then

        reconsider Y as Subset of NAT ;

        consider n be Nat such that

         A26: for k be Nat st k in Y holds k <= n by A25, STIRL2_1: 56;

        set n1 = (n + 1);



         A27: x in (R . n1) by A21, KURATO_0: 3;

        consider Sn be Subset-Family of T such that

         A28: Sn c= F and

         A29: Sn = { (S . j) where j be Element of NAT : j >= n1 } and

         A30: (R . n1) = ( Cl ( union Sn)) by A5;

        ( Cl ( union Sn)) = ( union ( clf Sn)) by A19, A28, PCOMPS_1: 9, PCOMPS_1: 20;

        then

        consider CLF be set such that

         A31: x in CLF and

         A32: CLF in ( clf Sn) by A30, A27, TARSKI:def 4;

        reconsider CLF as Subset of T by A32;

        consider U be Subset of T such that

         A33: CLF = ( Cl U) and

         A34: U in Sn by A32, PCOMPS_1:def 2;

        consider j be Element of NAT such that

         A35: U = (S . j) and

         A36: j >= n1 by A29, A34;



         A37: (Sp . j) in rngS;

        (Sp . j) meets W by A22, A23, A31, A33, A35, TOPS_1: 12;

        then

         A38: (Sp . j) in X by A37;

        ((S " ) . (S . j)) = j by A20, FUNCT_2: 26;

        then j in Y by A38;

        then j <= n by A26;

        hence thesis by A36, NAT_1: 13;

      end;

      let i;

      i in NAT by ORDINAL1:def 12;

      then ex SS be Subset-Family of T st SS c= F & SS = { (S . j) where j be Element of NAT : j >= i } & (R . i) = ( Cl ( union SS)) by A5;

      hence thesis;

    end;



     Lm2: for T be non empty TopSpace st T is countably_compact holds for F be Subset-Family of T st F is locally_finite & F is with_non-empty_elements holds F is finite

    proof

      let T be non empty TopSpace such that

       A1: T is countably_compact;

      given F be Subset-Family of T such that

       A2: F is locally_finite and

       A3: F is with_non-empty_elements and

       A4: F is infinite;

      consider f be sequence of F such that

       A5: f is one-to-one by A4, DICKSON: 3;



       A6: ( rng f) c= F;

      reconsider f as SetSequence of T by A4, FUNCT_2: 7;

      now

        let x be object;

        assume x in ( dom f);

        then (f . x) in ( rng f) by FUNCT_1:def 3;

        hence (f . x) is non empty by A3, A6;

      end;

      then f is non-empty by FUNCT_1:def 9;

      then ex R be non-empty closed SetSequence of T st R is non-ascending & (F is locally_finite & f is one-to-one implies ( meet R) = {} ) & for i holds ex fi be Subset-Family of T st (R . i) = ( Cl ( union fi)) & fi = { (f . j) where j be Element of NAT : j >= i } by A6, Th23;

      hence thesis by A1, A2, A5, Th22;

    end;



     Lm3: for T be non empty TopSpace st for F be Subset-Family of T st F is locally_finite & F is with_non-empty_elements holds F is finite holds for F be Subset-Family of T st F is locally_finite & for A be Subset of T st A in F holds ( card A) = 1 holds F is finite

    proof

      let T be non empty TopSpace such that

       A1: for F be Subset-Family of T st F is locally_finite & F is with_non-empty_elements holds F is finite;

      let F be Subset-Family of T such that

       A2: F is locally_finite and

       A3: for A be Subset of T st A in F holds ( card A) = 1;

       not ( {} T) in F by A3, CARD_1: 27;

      then F is with_non-empty_elements by SETFAM_1:def 8;

      hence thesis by A1, A2;

    end;



     Lm4: for T be non empty TopSpace st for F be Subset-Family of T st F is locally_finite & for A be Subset of T st A in F holds ( card A) = 1 holds F is finite holds for A be Subset of T st A is infinite holds ( Der A) is non empty

    proof

      deffunc P( set) = ( meet $1);

      let T be non empty TopSpace such that

       A1: for F be Subset-Family of T st F is locally_finite & for A be Subset of T st A in F holds ( card A) = 1 holds F is finite;

      let A be Subset of T such that

       A2: A is infinite;

      set F = { {x} where x be Element of T : x in A };

      reconsider F as Subset-Family of T by RELSET_2: 16;

      set PP = { P(y) where y be Element of ( bool the carrier of T) : y in F };



       A3: A c= PP

      proof

        let y be object such that

         A4: y in A;

        reconsider y9 = y as Point of T by A4;

         {y9} in F by A4;

        then P({) in PP;

        hence thesis by SETFAM_1: 10;

      end;

      assume

       A5: ( Der A) is empty;



       A6: F is locally_finite

      proof

        let x be Point of T;

        consider U be open Subset of T such that

         A7: x in U and

         A8: for y be Point of T st y in (A /\ U) holds x = y by A5, TOPGEN_1: 17;

        set M = { V where V be Subset of T : V in F & V meets U };

        take U;

        M c= { {x}}

        proof



           A9: {x} in { {x}} by TARSKI:def 1;

          let v be object;

          assume v in M;

          then

          consider V be Subset of T such that

           A10: v = V and

           A11: V in F and

           A12: V meets U;

          consider y be Point of T such that

           A13: V = {y} and

           A14: y in A by A11;

          y in U by A12, A13, ZFMISC_1: 50;

          then y in (A /\ U) by A14, XBOOLE_0:def 4;

          hence thesis by A8, A10, A13, A9;

        end;

        hence thesis by A7;

      end;

      now

        let a be Subset of T;

        assume a in F;

        then ex y be Point of T st a = {y} & y in A;

        hence ( card a) = 1 by CARD_1: 30;

      end;

      then

       A15: F is finite by A1, A6;

      PP is finite from FRAENKEL:sch 21( A15);

      hence thesis by A2, A3;

    end;

    ::$Canceled

    theorem :: COMPL_SP:25



     Th24: for X be non empty set, F be SetSequence of X st F is non-ascending holds for S be sequence of X st for n holds (S . n) in (F . n) holds ( rng S) is finite implies ( meet F) is non empty

    proof

      let X be non empty set, F be SetSequence of X such that

       A1: F is non-ascending;

      let S be sequence of X such that

       A2: for n holds (S . n) in (F . n);



       A3: ( dom S) = NAT by FUNCT_2:def 1;

      assume ( rng S) is finite;

      then

      consider x be object such that x in ( rng S) and

       A4: (S " {x}) is infinite by A3, CARD_2: 101;

      now

        let n be Nat;

        ex i st x in (F . i) & i >= n

        proof

          assume

           A5: for i st x in (F . i) holds i < n;

          (S " {x}) c= ( Segm n)

          proof

            let y be object such that

             A6: y in (S " {x});

            reconsider i = y as Nat by A6;

            (S . i) in {x} by A6, FUNCT_1:def 7;

            then

             A7: (S . i) = x by TARSKI:def 1;

            (S . i) in (F . i) by A2;

            then i < n by A5, A7;

            hence thesis by NAT_1: 44;

          end;

          hence thesis by A4;

        end;

        then

        consider i such that

         A8: x in (F . i) and

         A9: i >= n;

        (F . i) c= (F . n) by A1, A9, PROB_1:def 4;

        hence x in (F . n) by A8;

      end;

      hence thesis by KURATO_0: 3;

    end;



     Lm5: for T be T_1 non empty TopSpace st for A be Subset of T st A is infinite countable holds ( Der A) is non empty holds T is countably_compact

    proof

      let T be T_1 non empty TopSpace such that

       A1: for A be Subset of T st A is infinite countable holds ( Der A) is non empty;

      assume not T is countably_compact;

      then

      consider S be non-empty closed SetSequence of T such that

       A2: S is non-ascending and

       A3: ( meet S) = {} by Th22;

      defpred P[ object, object] means $2 in (S . $1);



       A4: for x be object st x in NAT holds ex y be object st y in the carrier of T & P[x, y]

      proof

        let x be object;

        assume x in NAT ;

        then

        reconsider x9 = x as Element of NAT ;

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

        then (S . x9) is non empty by FUNCT_1:def 9;

        then

        consider y be object such that

         A5: y in (S . x9) by XBOOLE_0:def 1;

        take y;

        thus thesis by A5;

      end;

      consider F be sequence of T such that

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

      reconsider rngF = ( rng F) as Subset of T;



       A7: for n holds (F . n) in (S . n) by A6, ORDINAL1:def 12;

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

      then ( rng F) is countable by CARD_3: 93;

      then ( Der rngF) is non empty by A1, A2, A3, A7, Th24;

      then

      consider p be object such that

       A8: p in ( Der rngF) by XBOOLE_0:def 1;

      reconsider p as Point of T by A8;

      consider n be Nat such that

       A9: not p in (S . n) by A3, KURATO_0: 3;



       A10: p in ((S . n) ` ) by A9, XBOOLE_0:def 5;

      deffunc f( set) = (F . $1);

      set F1n = { f(i) where i be Element of NAT : i in (n + 1) };



       A11: F1n c= the carrier of T

      proof

        let x be object;

        assume x in F1n;

        then ex i be Element of NAT st x = (F . i) & i in (n + 1);

        hence thesis;

      end;



       A12: (n + 1) is finite;



       A13: F1n is finite from FRAENKEL:sch 21( A12);

      reconsider F1n as Subset of T by A11;

      set U = (((S . n) ` ) \ (F1n \ {p}));

      reconsider U as Subset of T;

      p in {p} by TARSKI:def 1;

      then not p in (F1n \ {p}) by XBOOLE_0:def 5;

      then

       A14: p in U by A10, XBOOLE_0:def 5;

      (S . n) is closed by Def6;

      then U is open by A13, FRECHET: 4;

      then

      consider q be Point of T such that

       A15: q in (rngF /\ U) and

       A16: q <> p by A8, A14, TOPGEN_1: 17;

      q in rngF by A15, XBOOLE_0:def 4;

      then

      consider i be object such that

       A17: i in ( dom F) and

       A18: (F . i) = q by FUNCT_1:def 3;

      reconsider i as Element of NAT by A17;

      per cases ;

        suppose i <= n;

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

        then i in ( Segm (n + 1)) by NAT_1: 44;

        then q in F1n by A18;

        then q in (F1n \ {p}) by A16, ZFMISC_1: 56;

        then not q in U by XBOOLE_0:def 5;

        hence contradiction by A15, XBOOLE_0:def 4;

      end;

        suppose i > n;

        then

         A19: (S . i) c= (S . n) by A2, PROB_1:def 4;

        q in (S . i) by A6, A18;

        then not q in ((S . n) ` ) by A19, XBOOLE_0:def 5;

        then not q in U by XBOOLE_0:def 5;

        hence contradiction by A15, XBOOLE_0:def 4;

      end;

    end;



     Lm6: for T be non empty TopSpace st for F be Subset-Family of T st F is locally_finite & for A be Subset of T st A in F holds ( card A) = 1 holds F is finite holds T is countably_compact

    proof

      deffunc P( set) = ( meet $1);

      let T be non empty TopSpace such that

       A1: for F be Subset-Family of T st F is locally_finite & for A be Subset of T st A in F holds ( card A) = 1 holds F is finite;

      assume not T is countably_compact;

      then

      consider S be non-empty closed SetSequence of T such that

       A2: S is non-ascending and

       A3: ( meet S) = {} by Th22;

      defpred P[ object, object] means $2 in (S . $1);



       A4: for x be object st x in NAT holds ex y be object st y in the carrier of T & P[x, y]

      proof

        let x be object;

        assume x in NAT ;

        then

        reconsider x9 = x as Element of NAT ;

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

        then (S . x9) is non empty by FUNCT_1:def 9;

        then

        consider y be object such that

         A5: y in (S . x9) by XBOOLE_0:def 1;

        take y;

        thus thesis by A5;

      end;

      consider F be sequence of T such that

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

      reconsider rngF = ( rng F) as Subset of T;

      set A = { {x} where x be Element of T : x in rngF };

      reconsider A as Subset-Family of T by RELSET_2: 16;



       A7: A is locally_finite

      proof

        deffunc f( set) = {(F . $1)};

        let x be Point of T;

        consider i be Nat such that

         A8: not x in (S . i) by A3, KURATO_0: 3;

        take Si9 = ((S . i) ` );

        (S . i) is closed by Def6;

        hence x in Si9 & Si9 is open by A8, SUBSET_1: 29;

        set meetS = { V where V be Subset of T : V in A & V meets Si9 };

        set SI = { f(j) where j be Element of NAT : j in i };



         A9: meetS c= SI

        proof

          let v be object;

          assume v in meetS;

          then

          consider V be Subset of T such that

           A10: V = v and

           A11: V in A and

           A12: V meets Si9;

          consider y be Point of T such that

           A13: V = {y} and

           A14: y in ( rng F) by A11;

          consider z be object such that

           A15: z in ( dom F) and

           A16: y = (F . z) by A14, FUNCT_1:def 3;

          reconsider z as Element of NAT by A15;

          z in ( Segm i)

          proof

            assume not z in ( Segm i);

            then z >= i by NAT_1: 44;

            then

             A17: (S . z) c= (S . i) by A2, PROB_1:def 4;



             A18: y in Si9 by A12, A13, ZFMISC_1: 50;

            y in (S . z) by A6, A16;

            hence thesis by A17, A18, XBOOLE_0:def 5;

          end;

          hence thesis by A10, A13, A16;

        end;



         A19: i is finite;

        SI is finite from FRAENKEL:sch 21( A19);

        hence thesis by A9;

      end;

      set PP = { P(y) where y be Element of ( bool the carrier of T) : y in A };



       A20: rngF c= PP

      proof

        let y be object such that

         A21: y in rngF;

        reconsider y9 = y as Point of T by A21;

         {y9} in A by A21;

        then P({) in PP;

        hence thesis by SETFAM_1: 10;

      end;



       A22: for n holds (F . n) in (S . n) by A6, ORDINAL1:def 12;

      now

        let a be Subset of T;

        assume a in A;

        then ex y be Point of T st a = {y} & y in rngF;

        hence ( card a) = 1 by CARD_1: 30;

      end;

      then

       A23: A is finite by A1, A7;

      PP is finite from FRAENKEL:sch 21( A23);

      hence thesis by A2, A3, A22, A20, Th24;

    end;

    theorem :: COMPL_SP:26



     Th25: for T be non empty TopSpace holds T is countably_compact iff for F be Subset-Family of T st F is locally_finite & F is with_non-empty_elements holds F is finite

    proof

      let T be non empty TopSpace;

      thus T is countably_compact implies for F be Subset-Family of T st F is locally_finite & F is with_non-empty_elements holds F is finite by Lm2;

      assume for F be Subset-Family of T st F is locally_finite & F is with_non-empty_elements holds F is finite;

      then for F be Subset-Family of T st F is locally_finite & for A be Subset of T st A in F holds ( card A) = 1 holds F is finite by Lm3;

      hence thesis by Lm6;

    end;

    theorem :: COMPL_SP:27



     Th26: for T be non empty TopSpace holds T is countably_compact iff for F be Subset-Family of T st F is locally_finite & for A be Subset of T st A in F holds ( card A) = 1 holds F is finite

    proof

      let T be non empty TopSpace;

      thus T is countably_compact implies for F be Subset-Family of T st F is locally_finite & for A be Subset of T st A in F holds ( card A) = 1 holds F is finite

      proof

        assume T is countably_compact;

        then for F be Subset-Family of T st F is locally_finite & F is with_non-empty_elements holds F is finite by Th25;

        hence thesis by Lm3;

      end;

      thus thesis by Lm6;

    end;

    theorem :: COMPL_SP:28



     Th27: for T be T_1 non empty TopSpace holds T is countably_compact iff for A be Subset of T st A is infinite holds ( Der A) is non empty

    proof

      let T be T_1 non empty TopSpace;

      thus T is countably_compact implies for A be Subset of T st A is infinite holds ( Der A) is non empty

      proof

        assume T is countably_compact;

        then for F be Subset-Family of T st F is locally_finite & for A be Subset of T st A in F holds ( card A) = 1 holds F is finite by Th26;

        hence thesis by Lm4;

      end;

      assume for A be Subset of T st A is infinite holds ( Der A) is non empty;

      then for A be Subset of T st A is infinite countable holds ( Der A) is non empty;

      hence thesis by Lm5;

    end;

    theorem :: COMPL_SP:29

    for T be T_1 non empty TopSpace holds T is countably_compact iff for A be Subset of T st A is infinite countable holds ( Der A) is non empty by Lm5, Th27;

    scheme :: COMPL_SP:sch1

    Th39 { X() -> non empty set , P[ set, set] } :

ex A be Subset of X() st (for x,y be Element of X() st x in A & y in A & x <> y holds P[x, y]) & for x be Element of X() holds ex y be Element of X() st y in A & not P[x, y]

      provided

       A1: for x,y be Element of X() holds P[x, y] iff P[y, x]

       and

       A2: for x be Element of X() holds not P[x, x];

      set bX = ( bool X());

      consider R be Relation such that

       A3: R well_orders X() by WELLORD2: 17;

      (R /\ [:X(), X():]) c= [:X(), X():] by XBOOLE_1: 17;

      then

      reconsider R2 = (R |_2 X()) as Relation of X() by WELLORD1:def 6;

      reconsider RS = RelStr (# X(), R2 #) as non empty RelStr;

      set cRS = the carrier of RS;

      defpred H[ object, object, object] means for p be Element of X(), f be PartFunc of cRS, bX st $1 = p & $2 = f holds ((for q be Element of X() st q in ( union ( rng f)) holds P[p, q]) implies $3 = (( union ( rng f)) \/ {p})) & ((ex q be Element of X() st q in ( union ( rng f)) & not P[p, q]) implies $3 = ( union ( rng f)));



       A4: for x,y be object st x in cRS & y in ( PFuncs (cRS,bX)) holds ex z be object st z in bX & H[x, y, z]

      proof

        let x,y be object such that

         A5: x in cRS and

         A6: y in ( PFuncs (cRS,bX));

        reconsider f = y as PartFunc of cRS, bX by A6, PARTFUN1: 46;

        reconsider p = x as Element of X() by A5;

        per cases ;

          suppose

           A7: for q be Element of X() st q in ( union ( rng f)) holds P[p, q];

          take (( union ( rng f)) \/ {p});

          thus thesis by A7;

        end;

          suppose

           A8: ex q be Element of X() st q in ( union ( rng f)) & not P[p, q];

          take ( union ( rng f));

          thus thesis by A8;

        end;

      end;

      consider h be Function of [:cRS, ( PFuncs (cRS,bX)):], bX such that

       A9: for x,y be object st x in cRS & y in ( PFuncs (cRS,bX)) holds H[x, y, (h . (x,y))] from BINOP_1:sch 1( A4);

      set IRS = the InternalRel of RS;



       A10: R2 well_orders X() by A3, PCOMPS_2: 1;

      then R2 is_well_founded_in X() by WELLORD1:def 5;

      then

       A11: RS is well_founded by WELLFND1:def 2;

      then

      consider f be Function of cRS, bX such that

       A12: f is_recursively_expressed_by h by WELLFND1: 11;

      defpred S[ set] means (f . $1) c= ((IRS -Seg $1) \/ {$1}) & ($1 in (f . $1) implies for r be Element of X() st r in ( union ( rng (f | (IRS -Seg $1)))) holds P[$1, r]) & ( not $1 in (f . $1) implies ex r be Element of X() st r in ( union ( rng (f | (IRS -Seg $1)))) & not P[$1, r]);

      reconsider rngf = ( rng f) as Subset of bX;

      take A = ( union rngf);



       A13: ( field R2) = X() by A3, PCOMPS_2: 1;

      then

       A14: R2 is well-ordering by A10, WELLORD1: 4;



       A15: for x be Element of RS st for y be Element of RS st y <> x & [y, x] in IRS holds S[y] holds S[x]

      proof

        let x be Element of RS such that

         A16: for y be Element of RS st y <> x & [y, x] in IRS holds S[y];

        set fIx = (f | (IRS -Seg x));



         A17: ( union ( rng fIx)) c= (IRS -Seg x)

        proof

          let y be object;

          assume y in ( union ( rng fIx));

          then

          consider z be set such that

           A18: y in z and

           A19: z in ( rng fIx) by TARSKI:def 4;

          consider t be object such that

           A20: t in ( dom fIx) and

           A21: (fIx . t) = z by A19, FUNCT_1:def 3;



           A22: t in (IRS -Seg x) by A20, RELAT_1: 57;

          reconsider t as Element of RS by A20;



           A23: {t} c= (IRS -Seg x) by A22, ZFMISC_1: 31;



           A24: [t, x] in IRS by A22, WELLORD1: 1;

          then (IRS -Seg t) c= (IRS -Seg x) by A13, A14, WELLORD1: 29;

          then

           A25: ((IRS -Seg t) \/ {t}) c= (IRS -Seg x) by A23, XBOOLE_1: 8;

          t <> x by A22, WELLORD1: 1;

          then

           A26: (f . t) c= ((IRS -Seg t) \/ {t}) by A16, A24;

          (fIx . t) = (f . t) by A20, FUNCT_1: 47;

          then y in ((IRS -Seg t) \/ {t}) by A18, A21, A26;

          hence thesis by A25;

        end;



         A27: fIx in ( PFuncs (cRS,bX)) by PARTFUN1: 45;



         A28: (f . x) = (h . (x,fIx)) by A12, WELLFND1:def 5;

        per cases ;

          suppose

           A29: for q be Element of X() st q in ( union ( rng fIx)) holds P[x, q];

          then

           A30: (f . x) = (( union ( rng fIx)) \/ {x}) by A9, A28, A27;

          hence (f . x) c= ((IRS -Seg x) \/ {x}) by A17, XBOOLE_1: 9;

          thus x in (f . x) implies for r be Element of X() st r in ( union ( rng (f | (IRS -Seg x)))) holds P[x, r] by A29;



           A31: x in {x} by TARSKI:def 1;

          assume not x in (f . x);

          hence thesis by A30, A31, XBOOLE_0:def 3;

        end;

          suppose

           A32: ex q be Element of X() st q in ( union ( rng fIx)) & not P[x, q];

          then

           A33: (f . x) c= (IRS -Seg x) by A9, A17, A28, A27;

          (IRS -Seg x) c= ((IRS -Seg x) \/ {x}) by XBOOLE_1: 7;

          hence (f . x) c= ((IRS -Seg x) \/ {x}) by A33;

          thus thesis by A32, A33, WELLORD1: 1;

        end;

      end;



       A34: for x be Element of RS holds S[x] from WELLFND1:sch 3( A15, A11);

      thus for x,y be Element of X() st x in A & y in A & x <> y holds P[x, y]

      proof

         A35:

        now

          let x be Element of X();

          assume x in A;

          then

          consider y such that

           A36: x in y and

           A37: y in ( rng f) by TARSKI:def 4;

          defpred T[ set] means x in (f . $1);

          consider z be object such that

           A38: z in ( dom f) and

           A39: (f . z) = y by A37, FUNCT_1:def 3;

          reconsider z as Element of RS by A38;



           A40: T[z] by A36, A39;

          consider p be Element of RS such that

           A41: T[p] and

           A42: not ex q be Element of RS st p <> q & T[q] & [q, p] in IRS from WELLFND1:sch 2( A40, A11);

          p = x

          proof

            set fIp = (f | (IRS -Seg p));



             A43: fIp in ( PFuncs (cRS,bX)) by PARTFUN1: 45;



             A44: (f . p) = (h . (p,fIp)) by A12, WELLFND1:def 5;

            assume

             A45: p <> x;

            now

              per cases ;

                suppose

                 A46: for q be Element of X() st q in ( union ( rng fIp)) holds P[p, q];



                 A47: not x in {p} by A45, TARSKI:def 1;

                (f . p) = (( union ( rng fIp)) \/ {p}) by A9, A44, A43, A46;

                hence x in ( union ( rng fIp)) by A41, A47, XBOOLE_0:def 3;

              end;

                suppose ex q be Element of X() st q in ( union ( rng fIp)) & not P[p, q];

                hence x in ( union ( rng fIp)) by A9, A41, A44, A43;

              end;

            end;

            then

            consider y9 be set such that

             A48: x in y9 and

             A49: y9 in ( rng fIp) by TARSKI:def 4;

            consider z9 be object such that

             A50: z9 in ( dom fIp) and

             A51: (fIp . z9) = y9 by A49, FUNCT_1:def 3;

            reconsider z9 as Point of RS by A50;



             A52: z9 in (IRS -Seg p) by A50, RELAT_1: 57;

            then

             A53: z9 <> p by WELLORD1: 1;



             A54: [z9, p] in IRS by A52, WELLORD1: 1;

             T[z9] by A48, A50, A51, FUNCT_1: 47;

            hence thesis by A42, A53, A54;

          end;

          hence x in (f . x) by A41;

        end;

         A55:

        now



           A56: ( dom f) = cRS by FUNCT_2:def 1;

          let x,y be Element of X() such that

           A57: x in A and

           A58: y in A and

           A59: x <> y and

           A60: [x, y] in IRS;



           A61: y in (f . y) by A35, A58;

          set fIy = (f | (IRS -Seg y));

          x in (IRS -Seg y) by A59, A60, WELLORD1: 1;

          then

           A62: x in ( dom fIy) by A56, RELAT_1: 57;

          then

           A63: (fIy . x) in ( rng fIy) by FUNCT_1:def 3;



           A64: (fIy . x) = (f . x) by A62, FUNCT_1: 47;

          x in (f . x) by A35, A57;

          then x in ( union ( rng fIy)) by A63, A64, TARSKI:def 4;

          then P[y, x] by A34, A61;

          hence P[x, y] by A1;

        end;

        let x,y be Element of X() such that

         A65: x in A and

         A66: y in A and

         A67: x <> y;

        R2 well_orders X() by A3, PCOMPS_2: 1;

        then R2 is_connected_in X() by WELLORD1:def 5;

        then [x, y] in IRS or [y, x] in IRS by A67, RELAT_2:def 6;

        then P[x, y] or P[y, x] by A55, A65, A66, A67;

        hence thesis by A1;

      end;

      let x be Element of X();

      per cases ;

        suppose

         A68: x in A;

        take x;

        thus thesis by A2, A68;

      end;

        suppose

         A69: not x in A;

         not x in (f . x)

        proof

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

          then

           A70: (f . x) in ( rng f) by FUNCT_1:def 3;

          assume x in (f . x);

          hence thesis by A69, A70, TARSKI:def 4;

        end;

        then

        consider r be Element of X() such that

         A71: r in ( union ( rng (f | (IRS -Seg x)))) and

         A72: not P[x, r] by A34;

        take r;

        ( union ( rng (f | (IRS -Seg x)))) c= A by RELAT_1: 70, ZFMISC_1: 77;

        hence thesis by A71, A72;

      end;

    end;

    scheme :: COMPL_SP:sch2

    Th39 { X() -> non empty set , P[ set, set] } :

ex A be Subset of X() st (for x,y be Element of X() st x in A & y in A & x <> y holds P[x, y]) & for x be Element of X() holds ex y be Element of X() st y in A & not P[x, y]

      provided

       A1: for x,y be Element of X() holds P[x, y] iff P[y, x]

       and

       A2: for x be Element of X() holds not P[x, x];

      set bX = ( bool X());

      consider R be Relation such that

       A3: R well_orders X() by WELLORD2: 17;

      (R /\ [:X(), X():]) c= [:X(), X():] by XBOOLE_1: 17;

      then

      reconsider R2 = (R |_2 X()) as Relation of X() by WELLORD1:def 6;

      reconsider RS = RelStr (# X(), R2 #) as non empty RelStr;

      set cRS = the carrier of RS;

      defpred H[ object, object, object] means for p be Element of X(), f be PartFunc of cRS, bX st $1 = p & $2 = f holds ((for q be Element of X() st q in ( union ( rng f)) holds P[p, q]) implies $3 = (( union ( rng f)) \/ {p})) & ((ex q be Element of X() st q in ( union ( rng f)) & not P[p, q]) implies $3 = ( union ( rng f)));



       A4: for x,y be object st x in cRS & y in ( PFuncs (cRS,bX)) holds ex z be object st z in bX & H[x, y, z]

      proof

        let x,y be object such that

         A5: x in cRS and

         A6: y in ( PFuncs (cRS,bX));

        reconsider f = y as PartFunc of cRS, bX by A6, PARTFUN1: 46;

        reconsider p = x as Element of X() by A5;

        per cases ;

          suppose

           A7: for q be Element of X() st q in ( union ( rng f)) holds P[p, q];

          take (( union ( rng f)) \/ {p});

          thus thesis by A7;

        end;

          suppose

           A8: ex q be Element of X() st q in ( union ( rng f)) & not P[p, q];

          take ( union ( rng f));

          thus thesis by A8;

        end;

      end;

      consider h be Function of [:cRS, ( PFuncs (cRS,bX)):], bX such that

       A9: for x,y be object st x in cRS & y in ( PFuncs (cRS,bX)) holds H[x, y, (h . (x,y))] from BINOP_1:sch 1( A4);

      set IRS = the InternalRel of RS;



       A10: R2 well_orders X() by A3, PCOMPS_2: 1;

      then R2 is_well_founded_in X() by WELLORD1:def 5;

      then

       A11: RS is well_founded by WELLFND1:def 2;

      then

      consider f be Function of cRS, bX such that

       A12: f is_recursively_expressed_by h by WELLFND1: 11;

      defpred S[ set] means (f . $1) c= ((IRS -Seg $1) \/ {$1}) & ($1 in (f . $1) implies for r be Element of X() st r in ( union ( rng (f | (IRS -Seg $1)))) holds P[$1, r]) & ( not $1 in (f . $1) implies ex r be Element of X() st r in ( union ( rng (f | (IRS -Seg $1)))) & not P[$1, r]);

      reconsider rngf = ( rng f) as Subset of bX;

      take A = ( union rngf);



       A13: ( field R2) = X() by A3, PCOMPS_2: 1;

      then

       A14: R2 is well-ordering by A10, WELLORD1: 4;



       A15: for x be Element of RS st for y be Element of RS st y <> x & [y, x] in IRS holds S[y] holds S[x]

      proof

        let x be Element of RS such that

         A16: for y be Element of RS st y <> x & [y, x] in IRS holds S[y];

        set fIx = (f | (IRS -Seg x));



         A17: ( union ( rng fIx)) c= (IRS -Seg x)

        proof

          let y be object;

          assume y in ( union ( rng fIx));

          then

          consider z be set such that

           A18: y in z and

           A19: z in ( rng fIx) by TARSKI:def 4;

          consider t be object such that

           A20: t in ( dom fIx) and

           A21: (fIx . t) = z by A19, FUNCT_1:def 3;



           A22: t in (IRS -Seg x) by A20, RELAT_1: 57;

          reconsider t as Element of RS by A20;



           A23: {t} c= (IRS -Seg x) by A22, ZFMISC_1: 31;



           A24: [t, x] in IRS by A22, WELLORD1: 1;

          then (IRS -Seg t) c= (IRS -Seg x) by A13, A14, WELLORD1: 29;

          then

           A25: ((IRS -Seg t) \/ {t}) c= (IRS -Seg x) by A23, XBOOLE_1: 8;

          t <> x by A22, WELLORD1: 1;

          then

           A26: (f . t) c= ((IRS -Seg t) \/ {t}) by A16, A24;

          (fIx . t) = (f . t) by A20, FUNCT_1: 47;

          then y in ((IRS -Seg t) \/ {t}) by A18, A21, A26;

          hence thesis by A25;

        end;



         A27: fIx in ( PFuncs (cRS,bX)) by PARTFUN1: 45;



         A28: (f . x) = (h . (x,fIx)) by A12, WELLFND1:def 5;

        per cases ;

          suppose

           A29: for q be Element of X() st q in ( union ( rng fIx)) holds P[x, q];

          then

           A30: (f . x) = (( union ( rng fIx)) \/ {x}) by A9, A28, A27;

          hence (f . x) c= ((IRS -Seg x) \/ {x}) by A17, XBOOLE_1: 9;

          thus x in (f . x) implies for r be Element of X() st r in ( union ( rng (f | (IRS -Seg x)))) holds P[x, r] by A29;



           A31: x in {x} by TARSKI:def 1;

          assume not x in (f . x);

          hence thesis by A30, A31, XBOOLE_0:def 3;

        end;

          suppose

           A32: ex q be Element of X() st q in ( union ( rng fIx)) & not P[x, q];

          then

           A33: (f . x) c= (IRS -Seg x) by A9, A17, A28, A27;

          (IRS -Seg x) c= ((IRS -Seg x) \/ {x}) by XBOOLE_1: 7;

          hence (f . x) c= ((IRS -Seg x) \/ {x}) by A33;

          thus thesis by A32, A33, WELLORD1: 1;

        end;

      end;



       A34: for x be Element of RS holds S[x] from WELLFND1:sch 3( A15, A11);

      thus for x,y be Element of X() st x in A & y in A & x <> y holds P[x, y]

      proof

         A35:

        now

          let x be Element of X();

          assume x in A;

          then

          consider y such that

           A36: x in y and

           A37: y in ( rng f) by TARSKI:def 4;

          defpred T[ set] means x in (f . $1);

          consider z be object such that

           A38: z in ( dom f) and

           A39: (f . z) = y by A37, FUNCT_1:def 3;

          reconsider z as Element of RS by A38;



           A40: T[z] by A36, A39;

          consider p be Element of RS such that

           A41: T[p] and

           A42: not ex q be Element of RS st p <> q & T[q] & [q, p] in IRS from WELLFND1:sch 2( A40, A11);

          p = x

          proof

            set fIp = (f | (IRS -Seg p));



             A43: fIp in ( PFuncs (cRS,bX)) by PARTFUN1: 45;



             A44: (f . p) = (h . (p,fIp)) by A12, WELLFND1:def 5;

            assume

             A45: p <> x;

            now

              per cases ;

                suppose

                 A46: for q be Element of X() st q in ( union ( rng fIp)) holds P[p, q];



                 A47: not x in {p} by A45, TARSKI:def 1;

                (f . p) = (( union ( rng fIp)) \/ {p}) by A9, A44, A43, A46;

                hence x in ( union ( rng fIp)) by A41, A47, XBOOLE_0:def 3;

              end;

                suppose ex q be Element of X() st q in ( union ( rng fIp)) & not P[p, q];

                hence x in ( union ( rng fIp)) by A9, A41, A44, A43;

              end;

            end;

            then

            consider y9 be set such that

             A48: x in y9 and

             A49: y9 in ( rng fIp) by TARSKI:def 4;

            consider z9 be object such that

             A50: z9 in ( dom fIp) and

             A51: (fIp . z9) = y9 by A49, FUNCT_1:def 3;

            reconsider z9 as Point of RS by A50;



             A52: z9 in (IRS -Seg p) by A50, RELAT_1: 57;

            then

             A53: z9 <> p by WELLORD1: 1;



             A54: [z9, p] in IRS by A52, WELLORD1: 1;

             T[z9] by A48, A50, A51, FUNCT_1: 47;

            hence thesis by A42, A53, A54;

          end;

          hence x in (f . x) by A41;

        end;

         A55:

        now



           A56: ( dom f) = cRS by FUNCT_2:def 1;

          let x,y be Element of X() such that

           A57: x in A and

           A58: y in A and

           A59: x <> y and

           A60: [x, y] in IRS;



           A61: y in (f . y) by A35, A58;

          set fIy = (f | (IRS -Seg y));

          x in (IRS -Seg y) by A59, A60, WELLORD1: 1;

          then

           A62: x in ( dom fIy) by A56, RELAT_1: 57;

          then

           A63: (fIy . x) in ( rng fIy) by FUNCT_1:def 3;



           A64: (fIy . x) = (f . x) by A62, FUNCT_1: 47;

          x in (f . x) by A35, A57;

          then x in ( union ( rng fIy)) by A63, A64, TARSKI:def 4;

          then P[y, x] by A34, A61;

          hence P[x, y] by A1;

        end;

        let x,y be Element of X() such that

         A65: x in A and

         A66: y in A and

         A67: x <> y;

        R2 well_orders X() by A3, PCOMPS_2: 1;

        then R2 is_connected_in X() by WELLORD1:def 5;

        then [x, y] in IRS or [y, x] in IRS by A67, RELAT_2:def 6;

        then P[x, y] or P[y, x] by A55, A65, A66, A67;

        hence thesis by A1;

      end;

      let x be Element of X();

      per cases ;

        suppose

         A68: x in A;

        take x;

        thus thesis by A2, A68;

      end;

        suppose

         A69: not x in A;

         not x in (f . x)

        proof

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

          then

           A70: (f . x) in ( rng f) by FUNCT_1:def 3;

          assume x in (f . x);

          hence thesis by A69, A70, TARSKI:def 4;

        end;

        then

        consider r be Element of X() such that

         A71: r in ( union ( rng (f | (IRS -Seg x)))) and

         A72: not P[x, r] by A34;

        take r;

        ( union ( rng (f | (IRS -Seg x)))) c= A by RELAT_1: 70, ZFMISC_1: 77;

        hence thesis by A71, A72;

      end;

    end;

    theorem :: COMPL_SP:30



     Th29: for M be Reflexive symmetric non empty MetrStruct holds for r be Real st r > 0 holds ex A be Subset of M st (for p,q be Point of M st p <> q & p in A & q in A holds ( dist (p,q)) >= r) & for p be Point of M holds ex q be Point of M st q in A & p in ( Ball (q,r))

    proof

      let M be Reflexive symmetric non empty MetrStruct;

      let r be Real such that

       A1: r > 0 ;

      set cM = the carrier of M;

      defpred P[ set, set] means for p,q be Point of M st p = $1 & q = $2 holds ( dist (p,q)) >= r;



       A2: for x be Element of cM holds not P[x, x]

      proof

        let x be Element of cM;

        ( dist (x,x)) = 0 by METRIC_1: 1;

        hence thesis by A1;

      end;



       A3: for x,y be Element of cM holds P[x, y] iff P[y, x];

      consider A be Subset of cM such that

       A4: for x,y be Element of cM st x in A & y in A & x <> y holds P[x, y] and

       A5: for x be Element of cM holds ex y be Element of cM st y in A & not P[x, y] from Th39( A3, A2);

      take A;

      thus for p,q be Point of M st p <> q & p in A & q in A holds ( dist (p,q)) >= r by A4;

      let p be Point of M;

      consider y be Element of cM such that

       A6: y in A and

       A7: not P[p, y] by A5;

      take y;

      thus thesis by A6, A7, METRIC_1: 11;

    end;

    theorem :: COMPL_SP:31



     Th30: for M be Reflexive symmetric triangle non empty MetrStruct holds M is totally_bounded iff for r be Real, A be Subset of M st r > 0 & for p,q be Point of M st p <> q & p in A & q in A holds ( dist (p,q)) >= r holds A is finite

    proof

      let M be Reflexive symmetric triangle non empty MetrStruct;

      thus M is totally_bounded implies for r be Real, A be Subset of M st r > 0 & for p,q be Point of M st p <> q & p in A & q in A holds ( dist (p,q)) >= r holds A is finite

      proof

        assume

         A1: M is totally_bounded;

        let r be Real, A be Subset of M such that

         A2: r > 0 and

         A3: for p,q be Point of M st p <> q & p in A & q in A holds ( dist (p,q)) >= r;

        (r / 2) > 0 by A2, XREAL_1: 215;

        then

        consider G be Subset-Family of M such that

         A4: G is finite and

         A5: the carrier of M = ( union G) and

         A6: for C be Subset of M st C in G holds ex w be Point of M st C = ( Ball (w,(r / 2))) by A1;

        defpred f[ object, object] means ex D2 be set st D2 = $2 & $1 in D2 & $2 in G;



         A7: for x be object st x in A holds ex y be object st y in ( bool the carrier of M) & f[x, y]

        proof

          let x be object;

          assume x in A;

          then

          consider y such that

           A8: x in y and

           A9: y in G by A5, TARSKI:def 4;

          reconsider y as Subset of M by A9;

          take y;

          thus thesis by A8, A9;

        end;

        consider F be Function of A, ( bool the carrier of M) such that

         A10: for x be object st x in A holds f[x, (F . x)] from FUNCT_2:sch 1( A7);

        now

          let x1,x2 be object such that

           A11: x1 in A and

           A12: x2 in A and

           A13: (F . x1) = (F . x2);

          reconsider p1 = x1, p2 = x2 as Point of M by A11, A12;



           A14: f[x1, (F . x1)] by A10, A11;

          then (F . x1) in G;

          then

          consider w be Point of M such that

           A15: (F . x1) = ( Ball (w,(r / 2))) by A6;

          p1 in ( Ball (w,(r / 2))) by A15, A14;

          then

           A16: ( dist (p1,w)) < (r / 2) by METRIC_1: 11;



           A17: ( dist (p1,p2)) <= (( dist (p1,w)) + ( dist (w,p2))) by METRIC_1: 4;

           f[x2, (F . x2)] by A10, A12;

          then p2 in ( Ball (w,(r / 2))) by A13, A15;

          then ( dist (w,p2)) < (r / 2) by METRIC_1: 11;

          then (( dist (p1,w)) + ( dist (w,p2))) < ((r / 2) + (r / 2)) by A16, XREAL_1: 8;

          then ( dist (p1,p2)) < ((r / 2) + (r / 2)) by A17, XXREAL_0: 2;

          hence x1 = x2 by A3, A11, A12;

        end;

        then

         A18: F is one-to-one by FUNCT_2: 19;



         A19: ( rng F) c= G

        proof

          let x be object;

          assume x in ( rng F);

          then

          consider y be object such that

           A20: y in ( dom F) & x = (F . y) by FUNCT_1:def 3;

           f[y, (F . y)] by A10, A20;

          then

          consider D2 be set such that

           A21: D2 = (F . y) & y in D2 & (F . y) in G;

          thus thesis by A20, A21;

        end;

        ( dom F) = A by FUNCT_2:def 1;

        then (A,( rng F)) are_equipotent by A18, WELLORD2:def 4;

        hence thesis by A4, A19, CARD_1: 38;

      end;

      assume

       A22: for r be Real, A be Subset of M st r > 0 & for p,q be Point of M st p <> q & p in A & q in A holds ( dist (p,q)) >= r holds A is finite;

      let r such that

       A23: r > 0 ;

      reconsider r as Real;

      consider A be Subset of M such that

       A24: for p,q be Point of M st p <> q & p in A & q in A holds ( dist (p,q)) >= r and

       A25: for p be Point of M holds ex q be Point of M st q in A & p in ( Ball (q,r)) by A23, Th29;

      deffunc B( Point of M) = ( Ball ($1,r));

      set BA = { B(p) where p be Point of M : p in A };



       A26: A is finite by A22, A23, A24;



       A27: BA is finite from FRAENKEL:sch 21( A26);

      BA c= ( bool the carrier of M)

      proof

        let x be object;

        assume x in BA;

        then ex p be Point of M st x = B(p) & p in A;

        hence thesis;

      end;

      then

      reconsider BA as Subset-Family of M;

      take BA;

      the carrier of M c= ( union BA)

      proof

        let x be object;

        assume x in the carrier of M;

        then

        reconsider p = x as Point of M;

        consider q be Point of M such that

         A28: q in A and

         A29: p in B(q) by A25;

         B(q) in BA by A28;

        hence thesis by A29, TARSKI:def 4;

      end;

      hence BA is finite & ( union BA) = the carrier of M by A27, XBOOLE_0:def 10;

      let C be Subset of M;

      assume C in BA;

      then ex p be Point of M st C = B(p) & p in A;

      hence thesis;

    end;



     Lm7: for M be Reflexive symmetric triangle non empty MetrStruct holds for r be Real, A be Subset of M st r > 0 & for p,q be Point of M st p <> q & p in A & q in A holds ( dist (p,q)) >= r holds for F be Subset-Family of ( TopSpaceMetr M) st F = { {x} where x be Element of ( TopSpaceMetr M) : x in A } holds F is locally_finite

    proof

      let M be Reflexive symmetric triangle non empty MetrStruct;

      set T = ( TopSpaceMetr M);

      let r be Real, A be Subset of M such that

       A1: r > 0 and

       A2: for p,q be Point of M st p <> q & p in A & q in A holds ( dist (p,q)) >= r;



       A3: (r / 2) > 0 by A1, XREAL_1: 215;

      let F be Subset-Family of T such that

       A4: F = { {x} where x be Element of T : x in A };

      let x be Point of T;

      reconsider x9 = x as Point of M;

      reconsider B = ( Ball (x9,(r / 2))) as Subset of T;

      take B;



       A5: ( dist (x9,x9)) = 0 by METRIC_1: 1;

      B in ( Family_open_set M) by PCOMPS_1: 29;

      hence x in B & B is open by A5, A3, METRIC_1: 11, PRE_TOPC:def 2;

      set VV = { V where V be Subset of T : V in F & V meets B };

      per cases ;

        suppose

         A6: for p be Point of M st p in A holds ( dist (p,x9)) >= (r / 2);

        VV is empty

        proof

          assume VV is non empty;

          then

          consider v be object such that

           A7: v in VV by XBOOLE_0:def 1;

          consider V be Subset of T such that v = V and

           A8: V in F and

           A9: V meets B by A7;

          consider y be Point of T such that

           A10: V = {y} and

           A11: y in A by A4, A8;

          reconsider y as Point of M;

          y in B by A9, A10, ZFMISC_1: 50;

          then ( dist (x9,y)) < (r / 2) by METRIC_1: 11;

          hence thesis by A6, A11;

        end;

        hence thesis;

      end;

        suppose ex p be Point of M st p in A & ( dist (p,x9)) < (r / 2);

        then

        consider p be Point of M such that

         A12: p in A and

         A13: ( dist (p,x9)) < (r / 2);

        VV c= { {p}}

        proof

          let v be object;

          assume v in VV;

          then

          consider V be Subset of T such that

           A14: v = V and

           A15: V in F and

           A16: V meets B;

          consider y be Point of T such that

           A17: V = {y} and

           A18: y in A by A4, A15;

          reconsider y as Point of M;

          y in B by A16, A17, ZFMISC_1: 50;

          then ( dist (x9,y)) < (r / 2) by METRIC_1: 11;

          then

           A19: (( dist (p,x9)) + ( dist (x9,y))) < ((r / 2) + (r / 2)) by A13, XREAL_1: 8;

          ( dist (p,y)) <= (( dist (p,x9)) + ( dist (x9,y))) by METRIC_1: 4;

          then ( dist (p,y)) < ((r / 2) + (r / 2)) by A19, XXREAL_0: 2;

          then p = y by A2, A12, A18;

          hence thesis by A14, A17, TARSKI:def 1;

        end;

        hence thesis;

      end;

    end;

    theorem :: COMPL_SP:32



     Th31: for M be Reflexive symmetric triangle non empty MetrStruct st ( TopSpaceMetr M) is countably_compact holds M is totally_bounded

    proof

      deffunc P( set) = ( meet $1);

      let M be Reflexive symmetric triangle non empty MetrStruct such that

       A1: ( TopSpaceMetr M) is countably_compact;

      set T = ( TopSpaceMetr M);

      assume not M is totally_bounded;

      then

      consider r be Real, A be Subset of M such that

       A2: r > 0 and

       A3: for p,q be Point of M st p <> q & p in A & q in A holds ( dist (p,q)) >= r and

       A4: A is infinite by Th30;

      reconsider A as Subset of T;

      set F = { {x} where x be Element of T : x in A };

      reconsider F as Subset-Family of T by RELSET_2: 16;

       A5:

      now

        let a be Subset of T;

        assume a in F;

        then ex y be Point of T st a = {y} & y in A;

        hence ( card a) = 1 by CARD_1: 30;

      end;

      set PP = { P(y) where y be Subset of T : y in F };



       A6: A c= PP

      proof

        let y be object such that

         A7: y in A;

        reconsider y9 = y as Point of T by A7;

         {y9} in F by A7;

        then P({) in PP;

        hence thesis by SETFAM_1: 10;

      end;

      F is locally_finite by A2, A3, Lm7;

      then

       A8: F is finite by A1, A5, Th26;

      PP is finite from FRAENKEL:sch 21( A8);

      hence thesis by A4, A6;

    end;

    theorem :: COMPL_SP:33



     Th32: for M be non empty MetrSpace st M is totally_bounded holds ( TopSpaceMetr M) is second-countable

    proof

      let M be non empty MetrSpace such that

       A1: M is totally_bounded;

      set T = ( TopSpaceMetr M);

      defpred F[ object, object] means for i st i = $1 holds for G be Subset-Family of T st $2 = G holds G is finite & the carrier of M = ( union G) & for C be Subset of M st C in G holds ex w be Point of M st C = ( Ball (w,(1 / (i + 1))));



       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 i = x as Nat;

        (1 / (i + 1)) > 0 by XREAL_1: 139;

        then

        consider G be Subset-Family of T such that

         A3: G is finite and

         A4: the carrier of M = ( union G) and

         A5: for C be Subset of M st C in G holds ex w be Point of M st C = ( Ball (w,(1 / (i + 1)))) by A1;

        take G;

        thus thesis by A3, A4, A5;

      end;

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

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

      set U = ( Union f);



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



       A8: for A be Subset of T st A is open holds for p be Point of T st p in A holds ex a be Subset of T st a in U & p in a & a c= A

      proof

        let A be Subset of T such that

         A9: A is open;

        let p be Point of T such that

         A10: p in A;

        reconsider p9 = p as Point of M;

        consider r be Real such that

         A11: r > 0 and

         A12: ( Ball (p9,r)) c= A by A9, A10, TOPMETR: 15;

        reconsider r as Real;

        consider n be Nat such that

         A13: n > 0 and

         A14: (1 / n) < (r / 2) by A11, UNIFORM1: 1, XREAL_1: 215;



         A15: ((1 / n) + (1 / n)) < ((r / 2) + (r / 2)) by A14, XREAL_1: 8;

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

        reconsider fn = (f . n1) as Subset-Family of T;

        the carrier of M = ( union fn) by A6;

        then

        consider x be set such that

         A16: p in x and

         A17: x in fn by TARSKI:def 4;

        reconsider x as Subset of M by A17;

        consider w be Point of M such that

         A18: x = ( Ball (w,(1 / (n1 + 1)))) by A6, A17;

        reconsider B = ( Ball (w,(1 / n))) as Subset of T;

        take B;

        (f . n1) in ( rng f) by A7, FUNCT_1:def 3;

        then B in ( union ( rng f)) by A17, A18, TARSKI:def 4;

        hence B in U & p in B by A16, A18, CARD_3:def 4;

        let q be object such that

         A19: q in B;

        reconsider q9 = q as Point of M by A19;



         A20: ( dist (q9,w)) < (1 / n) by A19, METRIC_1: 11;

        ( dist (w,p9)) < (1 / (n1 + 1)) by A16, A18, METRIC_1: 11;

        then

         A21: (( dist (q9,w)) + ( dist (w,p9))) < ((1 / n) + (1 / n)) by A20, XREAL_1: 8;

        ( dist (q9,p9)) <= (( dist (q9,w)) + ( dist (w,p9))) by METRIC_1: 4;

        then ( dist (q9,p9)) < ((1 / n) + (1 / n)) by A21, XXREAL_0: 2;

        then ( dist (q9,p9)) < ((r / 2) + (r / 2)) by A15, XXREAL_0: 2;

        then q in ( Ball (p9,r)) by METRIC_1: 11;

        hence thesis by A12;

      end;

      set CB = the set of all ( card B) where B be Basis of T;

      U c= the topology of T

      proof

        let x be object;

        assume x in U;

        then x in ( union ( rng f)) by CARD_3:def 4;

        then

        consider y such that

         A22: x in y and

         A23: y in ( rng f) by TARSKI:def 4;

        reconsider X = x as Subset of T by A22, A23;

        consider z be object such that

         A24: z in ( dom f) and

         A25: (f . z) = y by A23, FUNCT_1:def 3;

        reconsider z as Element of NAT by A24;

        (f . z) = y by A25;

        then ex w be Point of M st X = ( Ball (w,(1 / (z + 1)))) by A6, A22;

        hence thesis by PCOMPS_1: 29;

      end;

      then U is Basis of T by A8, YELLOW_9: 32;

      then

       A26: ( card U) in CB;

      now

        let x;

        assume x in ( dom f);

        then

        reconsider i = x as Element of NAT ;

        reconsider fx = (f . i) as Subset-Family of T;

        fx is finite by A6;

        hence (f . x) is countable by CARD_4: 1;

      end;

      then U is countable by A7, CARD_4: 2, CARD_4: 11;

      then

       A27: ( card U) c= omega by CARD_3:def 14;

      ( weight T) = ( meet CB) by WAYBEL23:def 5;

      then ( weight T) c= ( card U) by A26, SETFAM_1: 3;

      then ( weight T) c= omega by A27;

      hence thesis by WAYBEL23:def 6;

    end;

    theorem :: COMPL_SP:34



     Th33: for T be non empty TopSpace holds T is second-countable implies for F be Subset-Family of T st F is Cover of T & F is open holds ex G be Subset-Family of T st G c= F & G is Cover of T & G is countable

    proof

      let T be non empty TopSpace;

      assume T is second-countable;

      then

      consider B be Basis of T such that

       A1: B is countable by TOPGEN_4: 57;



       A2: ( card B) c= omega by A1, CARD_3:def 14;

      let F be Subset-Family of T such that

       A3: F is Cover of T and

       A4: F is open;

      defpred P[ object, object] means ex D2 be set st D2 = $2 & for b be Subset of T st b = $1 holds ((ex y st y in F & b c= y) implies ($2 in F & b c= D2)) & ((for y st y in F holds not b c= y) implies $2 = {} );



       A5: for x be object st x in B holds ex y be object st y in ( bool the carrier of T) & P[x, y]

      proof

        let x be object;

        assume x in B;

        then

        reconsider b = x as Subset of T;

        per cases ;

          suppose ex y st y in F & b c= y;

          then

          consider y such that

           A6: y in F and

           A7: b c= y;

          reconsider y as Subset of T by A6;

          take y;

          thus y in ( bool the carrier of T);

          take y;

          thus thesis by A6, A7;

        end;

          suppose

           A8: for y st y in F holds not b c= y;

          take y = ( {} T);

          thus y in ( bool the carrier of T);

          take y;

          thus thesis by A8;

        end;

      end;

      consider p be Function of B, ( bool the carrier of T) such that

       A9: for x be object st x in B holds P[x, (p . x)] from FUNCT_2:sch 1( A5);

      take RNG = (( rng p) \ { {} });



       A10: ( dom p) = B by FUNCT_2:def 1;

      thus RNG c= F

      proof

        let y be object such that

         A11: y in RNG;

        y in ( rng p) by A11, XBOOLE_0:def 5;

        then

        consider z be object such that

         A12: z in ( dom p) and

         A13: (p . z) = y by FUNCT_1:def 3;

        reconsider z as Subset of T by A10, A12;



         A14: P[z, (p . z)] by A9, A12;

        (ex y st y in F & z c= y) or for y st y in F holds not z c= y;

        then (p . z) in F & z c= (p . z) or (p . z) = {} by A14;

        hence thesis by A11, A13, ZFMISC_1: 56;

      end;

      the carrier of T c= ( union RNG)

      proof

        let y be object;

        assume y in the carrier of T;

        then

        reconsider q = y as Point of T;

        consider W be Subset of T such that

         A15: q in W and

         A16: W in F by A3, PCOMPS_1: 3;

        W is open by A4, A16;

        then

        consider U be Subset of T such that

         A17: U in B and

         A18: q in U and

         A19: U c= W by A15, YELLOW_9: 31;



         A20: (p . U) in ( rng p) by A10, A17, FUNCT_1:def 3;

        then

        reconsider pU = (p . U) as Subset of T;

         P[U, (p . U)] by A9, A17;

        then

         A21: U c= pU by A16, A19;

        then pU in RNG by A18, A20, ZFMISC_1: 56;

        hence thesis by A18, A21, TARSKI:def 4;

      end;

      then ( [#] T) = ( union RNG) by XBOOLE_0:def 10;

      hence RNG is Cover of T by SETFAM_1: 45;

      ( card ( rng p)) c= ( card B) by A10, CARD_2: 61;

      then ( card ( rng p)) c= omega by A2;

      then ( rng p) is countable by CARD_3:def 14;

      hence thesis by CARD_3: 95;

    end;

    begin

    theorem :: COMPL_SP:35



     Th34: for M be non empty MetrSpace holds ( TopSpaceMetr M) is compact iff ( TopSpaceMetr M) is countably_compact

    proof

      let M be non empty MetrSpace;

      set T = ( TopSpaceMetr M);

      thus T is compact implies T is countably_compact;

      assume

       A1: T is countably_compact;

      let F be Subset-Family of T such that

       A2: F is Cover of T and

       A3: F is open;

      M is totally_bounded by A1, Th31;

      then T is second-countable by Th32;

      then

      consider G be Subset-Family of T such that

       A4: G c= F and

       A5: G is Cover of T and

       A6: G is countable by A2, A3, Th33;

      G is open by A3, A4;

      then ex H be Subset-Family of T st H c= G & H is Cover of T & H is finite by A1, A5, A6;

      hence thesis by A4, XBOOLE_1: 1;

    end;

    theorem :: COMPL_SP:36



     Th35: for X be set, F be Subset-Family of X st F is finite holds for A be Subset of X st A is infinite & A c= ( union F) holds ex Y be Subset of X st Y in F & (Y /\ A) is infinite

    proof

      defpred P[ object, object] means ex D2 be set st D2 = $2 & $1 in D2;

      let X be set, F be Subset-Family of X such that

       A1: F is finite;

      let A be Subset of X such that

       A2: A is infinite and

       A3: A c= ( union F);

      set I = ( INTERSECTION (F, {A}));

      ( card [:F, {A}:]) = ( card F) by CARD_1: 69;

      then ( card I) c= ( card F) by TOPGEN_4: 25;

      then

       A4: I is finite by A1;



       A5: for x be object st x in A holds ex y be object st y in I & P[x, y]

      proof

        let x be object such that

         A6: x in A;

        consider y such that

         A7: x in y and

         A8: y in F by A3, A6, TARSKI:def 4;

        take (y /\ A);

        A in {A} by TARSKI:def 1;

        hence (y /\ A) in I by A8, SETFAM_1:def 5;

        take (y /\ A);

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

      end;

      consider p be Function of A, I such that

       A9: for x be object st x in A holds P[x, (p . x)] from FUNCT_2:sch 1( A5);

      consider x be object such that

       A10: x in A by A2, XBOOLE_0:def 1;

      ex y be object st y in I & P[x, y] by A5, A10;

      then ( dom p) = A by FUNCT_2:def 1;

      then

      consider t be object such that

       A11: t in ( rng p) and

       A12: (p " {t}) is infinite by A2, A4, CARD_2: 101;

      consider Y,Z be set such that

       A13: Y in F and

       A14: Z in {A} and

       A15: t = (Y /\ Z) by A11, SETFAM_1:def 5;

      reconsider Y as Subset of X by A13;

      take Y;



       A16: Z = A by A14, TARSKI:def 1;

      (p " {t}) c= (Y /\ A)

      proof

        let z be object such that

         A17: z in (p " {t});

        (p . z) in {t} by A17, FUNCT_1:def 7;

        then

         A18: (p . z) = t by TARSKI:def 1;

         P[z, (p . z)] by A9, A17;

        hence thesis by A15, A16, A18;

      end;

      hence thesis by A12, A13;

    end;

    theorem :: COMPL_SP:37

    for M be non empty MetrSpace holds ( TopSpaceMetr M) is compact iff M is totally_bounded & M is complete

    proof

      let M be non empty MetrSpace;

      set T = ( TopSpaceMetr M);

      thus T is compact implies M is totally_bounded & M is complete by TBSP_1: 8, TBSP_1: 9;

      assume that

       A1: M is totally_bounded and

       A2: M is complete;

      now

        reconsider NULL = 0 as Real;

        deffunc F( Nat) = (1 / (1 + $1));

        set cM = the carrier of M;

        defpred P[ object, object] means for a,b be Subset of M st $1 = a & $2 = b holds b c= a & ( diameter b) <= (( diameter a) / 2);

        defpred Q[ object] means for a be Subset of M st a = $1 holds a is bounded & a is infinite & a is closed;

        consider seq be Real_Sequence such that

         A3: for n be Nat holds (seq . n) = F(n) from SEQ_1:sch 1;

        set Ns = (NULL (#) seq);



         A4: for x be object st x in ( bool cM) & Q[x] holds ex y be object st y in ( bool cM) & P[x, y] & Q[y]

        proof

          let x be object such that

           A5: x in ( bool cM) and

           A6: Q[x];

          reconsider X = x as Subset of M by A5;

          reconsider X9 = X as Subset of T;

          set d = ( diameter X);

          per cases by A6, TBSP_1: 21;

            suppose

             A7: d = 0 ;

            take Y = X;

            thus thesis by A6, A7;

          end;

            suppose

             A8: d > 0 ;

            then (d / 4) > 0 by XREAL_1: 224;

            then

            consider F be Subset-Family of M such that

             A9: F is finite and

             A10: cM = ( union F) and

             A11: for C be Subset of M st C in F holds ex w be Point of M st C = ( Ball (w,(d / 4))) by A1;

            X is infinite by A6;

            then

            consider Y be Subset of M such that

             A12: Y in F and

             A13: (Y /\ X) is infinite by A9, A10, Th35;

            set YX = (Y /\ X);



             A14: ex w be Point of M st Y = ( Ball (w,(d / 4))) by A11, A12;

            then

             A15: Y is bounded;

            then

             A16: ( diameter YX) <= ( diameter Y) by TBSP_1: 24, XBOOLE_1: 17;

            ( diameter Y) <= (2 * (d / 4)) by A8, A14, TBSP_1: 23, XREAL_1: 224;

            then

             A17: ( diameter YX) <= (d / 2) by A16, XXREAL_0: 2;

            reconsider yx = YX as Subset of T;

            reconsider CYX = ( Cl yx) as Subset of M;

            take CYX;



             A18: yx c= ( Cl yx) by PRE_TOPC: 18;



             A19: yx c= X9 by XBOOLE_1: 17;

            X is closed by A6;

            then

             A20: X9 is closed by Th6;

            YX is bounded by A15, TBSP_1: 14, XBOOLE_1: 17;

            hence thesis by A13, A17, A18, A20, A19, Th6, Th8, TOPS_1: 5;

          end;

        end;

        consider G be Subset-Family of M such that

         A21: G is finite and

         A22: the carrier of M = ( union G) and

         A23: for C be Subset of M st C in G holds ex w be Point of M st C = ( Ball (w,(1 / 2))) by A1;

        let A be Subset of T;

        assume A is infinite;

        then

        consider X be Subset of M such that

         A24: X in G and

         A25: (X /\ A) is infinite by A21, A22, Th35;

        reconsider XA = (X /\ A) as Subset of M;

        reconsider xa = XA as Subset of T;

        reconsider CXA = ( Cl xa) as Subset of M;



         A26: XA is bounded & ( diameter XA) <= 1

        proof



           A27: ex w be Point of M st X = ( Ball (w,(1 / 2))) by A23, A24;

          then

           A28: ( diameter X) <= (2 * (1 / 2)) by TBSP_1: 23;



           A29: X is bounded by A27;

          then ( diameter XA) <= ( diameter X) by TBSP_1: 24, XBOOLE_1: 17;

          hence thesis by A29, A28, TBSP_1: 14, XBOOLE_1: 17, XXREAL_0: 2;

        end;

        then CXA is bounded by Th8;

        then

         A30: 0 <= ( diameter CXA) by TBSP_1: 21;

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

        then

         A31: CXA in ( bool cM) & Q[CXA] by A25, A26, Th6, Th8;

        consider f be Function such that

         A32: ( dom f) = NAT & ( rng f) c= ( bool cM) and

         A33: (f . 0 ) = CXA and

         A34: for k be Nat holds P[(f . k), (f . (k + 1))] & Q[(f . k)] from TREES_2:sch 5( A31, A4);

        reconsider f as SetSequence of M by A32, FUNCT_2: 2;



         A35: for n holds (f . n) is bounded by A34;

         A36:

        now

          let x be object;

          assume x in ( dom f);

          then

          reconsider i = x as Element of NAT ;

          (f . i) is infinite by A34;

          hence (f . x) is non empty;

        end;

        for n holds (f . n) is closed by A34;

        then

        reconsider f as non-empty pointwise_bounded closed SetSequence of M by A36, A35, Def1, Def8, FUNCT_1:def 9;



         A37: (Ns . 0 ) = (NULL * (seq . 0 )) by SEQ_1: 9;

        for n be Nat holds (f . (n + 1)) c= (f . n) by A34;

        then

         A38: f is non-ascending by KURATO_0:def 3;

        set df = ( diameter f);

        defpred N[ Nat] means (Ns . $1) <= (df . $1) & (df . $1) <= (seq . $1);



         A39: for n be Nat st N[n] holds N[(n + 1)]

        proof

          let n be Nat;

          assume N[n];

          then (df . n) <= F(n) by A3;

          then

           A40: ((df . n) / 2) <= ( F(n) / 2) by XREAL_1: 72;

          set n1 = (n + 1);



           A41: ( diameter (f . n)) = (df . n) by Def2;

          ( diameter (f . n1)) <= (( diameter (f . n)) / 2) by A34;

          then (df . n1) <= ((df . n) / 2) by A41, Def2;

          then

           A42: (df . n1) <= ( F(n) / 2) by A40, XXREAL_0: 2;



           A43: (Ns . n1) = (NULL * (seq . n1)) by SEQ_1: 9;

          (f . n1) is bounded by Def1;

          then

           A44: 0 <= ( diameter (f . n1)) by TBSP_1: 21;

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

          then

           A45: F(n1) >= (1 / (2 * n1)) by XREAL_1: 118;

          (1 / (2 * n1)) = ( F(n) / 2) by XCMPLX_1: 78;

          then F(n1) >= (df . n1) by A42, A45, XXREAL_0: 2;

          hence thesis by A3, A44, A43, Def2;

        end;



         A46: (seq . 0 ) = (1 / (1 + 0 )) by A3;



         A47: for n be Nat holds (seq . n) = (1 / (n + 1)) by A3;

        then

         A48: seq is convergent by SEQ_4: 31;

        ( diameter CXA) <= 1 by A26, Th8;

        then

         A49: N[ 0 ] by A33, A30, A46, A37, Def2;



         A50: for n be Nat holds N[n] from NAT_1:sch 2( A49, A39);



         A51: Ns is convergent by A47, SEQ_2: 7, SEQ_4: 31;



         A52: ( lim seq) = 0 by A47, SEQ_4: 31;

        then

         A53: ( lim Ns) = (NULL * 0 ) by A47, SEQ_2: 8, SEQ_4: 31;

        then

         A54: ( lim df) = 0 by A48, A52, A51, A50, SEQ_2: 20;

        then ( meet f) is non empty by A2, A38, Th10;

        then

        consider p be object such that

         A55: p in ( meet f) by XBOOLE_0:def 1;

        reconsider p as Point of T by A55;

        reconsider p9 = p as Point of M;



         A56: df is convergent by A48, A52, A51, A53, A50, SEQ_2: 19;

        now

          let U be open Subset of T;

          assume p in U;

          then

          consider r be Real such that

           A57: r > 0 and

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

          (r / 2) > 0 by A57, XREAL_1: 215;

          then

          consider n be Nat such that

           A59: for m be Nat st n <= m holds |.((df . m) - 0 ).| < (r / 2) by A54, A56, SEQ_2:def 7;

          p in (f . n) by A55, KURATO_0: 3;

          then

           A60: {p} c= (f . n) by ZFMISC_1: 31;

          (f . n) is infinite by A34;

          then {p} c< (f . n) by A60, XBOOLE_0:def 8;

          then ((f . n) \ {p}) <> {} by XBOOLE_1: 105;

          then

          consider q be object such that

           A61: q in ((f . n) \ {p}) by XBOOLE_0:def 1;

          reconsider q as Point of T by A61;



           A62: q in (f . n) by A61, ZFMISC_1: 56;



           A63: q in (f . n) by A61, ZFMISC_1: 56;

          reconsider q9 = q as Point of M;

          q <> p by A61, ZFMISC_1: 56;

          then

           A64: ( dist (p9,q9)) <> 0 by METRIC_1: 2;

          reconsider B = ( Ball (q9,( dist (p9,q9)))) as Subset of T;



           A65: ( dist (p9,q9)) >= 0 by METRIC_1: 5;

          ( dist (q9,q9)) = 0 by METRIC_1: 1;

          then

           A66: q in B by A64, A65, METRIC_1: 11;

          ( Ball (q9,( dist (p9,q9)))) in ( Family_open_set M) by PCOMPS_1: 29;

          then

           A67: B is open by PRE_TOPC:def 2;

          (f . n) c= ( Cl xa) by A33, A38, PROB_1:def 4;

          then B meets xa by A67, A66, A62, PRE_TOPC: 24;

          then

          consider s be object such that

           A68: s in B and

           A69: s in xa by XBOOLE_0: 3;

          reconsider s as Point of M by A68;

          reconsider s9 = s as Point of T;

          take s9;



           A70: (Ns . n) = (NULL * (seq . n)) by SEQ_1: 9;



           A71: |.((df . n) - 0 ).| < (r / 2) by A59;



           A72: (f . n) is bounded by A34;

          (df . n) >= (Ns . n) by A50;

          then (df . n) < (r / 2) by A70, A71, ABSVALUE:def 1;

          then

           A73: ( diameter (f . n)) < (r / 2) by Def2;

          p in (f . n) by A55, KURATO_0: 3;

          then ( dist (p9,q9)) <= ( diameter (f . n)) by A63, A72, TBSP_1:def 8;

          then

           A74: ( dist (p9,q9)) < (r / 2) by A73, XXREAL_0: 2;

          ( dist (q9,s)) < ( dist (p9,q9)) by A68, METRIC_1: 11;

          then ( dist (q9,s)) < (r / 2) by A74, XXREAL_0: 2;

          then

           A75: (( dist (p9,q9)) + ( dist (q9,s))) < ((r / 2) + (r / 2)) by A74, XREAL_1: 8;

          ( dist (p9,s)) <= (( dist (p9,q9)) + ( dist (q9,s))) by METRIC_1: 4;

          then ( dist (p9,s)) < r by A75, XXREAL_0: 2;

          then

           A76: s in ( Ball (p9,r)) by METRIC_1: 11;

          s in A by A69, XBOOLE_0:def 4;

          hence s9 in (A /\ U) & s9 <> p by A58, A68, A76, METRIC_1: 11, XBOOLE_0:def 4;

        end;

        hence ( Der A) is non empty by TOPGEN_1: 17;

      end;

      then T is countably_compact by Th27;

      hence thesis by Th34;

    end;

    begin

    theorem :: COMPL_SP:38



     Th37: for M be MetrStruct, a be Point of M, x holds x in ( [:X, (the carrier of M \ {a}):] \/ { [X, a]}) iff ex y be set, b be Point of M st x = [y, b] & (y in X & b <> a or y = X & b = a)

    proof

      let M be MetrStruct, a be Point of M, x;

      thus x in ( [:X, (the carrier of M \ {a}):] \/ { [X, a]}) implies ex y be set, b be Point of M st x = [y, b] & (y in X & b <> a or y = X & b = a)

      proof

        assume

         A1: x in ( [:X, (the carrier of M \ {a}):] \/ { [X, a]});

        per cases by A1, XBOOLE_0:def 3;

          suppose x in [:X, (the carrier of M \ {a}):];

          then

          consider x1,x2 be object such that

           A2: x1 in X and

           A3: x2 in (the carrier of M \ {a}) and

           A4: x = [x1, x2] by ZFMISC_1:def 2;

          reconsider x2 as Point of M by A3;

          reconsider x1 as set by TARSKI: 1;

          take x1, x2;

          thus thesis by A2, A3, A4, ZFMISC_1: 56;

        end;

          suppose x in { [X, a]};

          then x = [X, a] by TARSKI:def 1;

          hence thesis;

        end;

      end;

      given y be set, b be Point of M such that

       A5: x = [y, b] and

       A6: y in X & b <> a or y = X & b = a;

      per cases by A6;

        suppose

         A7: y in X & b <> a;

        the carrier of M is non empty

        proof

          assume

           A8: the carrier of M is empty;

          then a = {} by SUBSET_1:def 1;

          hence thesis by A7, A8, SUBSET_1:def 1;

        end;

        then b in (the carrier of M \ {a}) by A7, ZFMISC_1: 56;

        then x in [:X, (the carrier of M \ {a}):] by A5, A7, ZFMISC_1: 87;

        hence thesis by XBOOLE_0:def 3;

      end;

        suppose y = X & b = a;

        then x in { [X, a]} by A5, TARSKI:def 1;

        hence thesis by XBOOLE_0:def 3;

      end;

    end;

    definition

      let M be MetrStruct;

      let a be Point of M;

      let X be set;

      :: COMPL_SP:def10

      func well_dist (a,X) -> Function of [:( [:X, (the carrier of M \ {a}):] \/ { [X, a]}), ( [:X, (the carrier of M \ {a}):] \/ { [X, a]}):], REAL means

      : Def10: for x,y be Element of ( [:X, (the carrier of M \ {a}):] \/ { [X, a]}) holds for x1,y1 be object, x2,y2 be Point of M st x = [x1, x2] & y = [y1, y2] holds (x1 = y1 implies (it . (x,y)) = ( dist (x2,y2))) & (x1 <> y1 implies (it . (x,y)) = (( dist (x2,a)) + ( dist (a,y2))));

      existence

      proof

        set XX = ( [:X, (the carrier of M \ {a}):] \/ { [X, a]});

        defpred P[ object, object, object] means for x,y be Element of XX st x = $1 & y = $2 holds for x1,y1 be object, x2,y2 be Point of M st x = [x1, x2] & y = [y1, y2] holds (x1 = y1 implies $3 = ( dist (x2,y2))) & (x1 <> y1 implies $3 = (( dist (x2,a)) + ( dist (a,y2))));



         A1: for x,y be object st x in XX & y in XX holds ex z be object st z in REAL & P[x, y, z]

        proof

          let x,y be object such that

           A2: x in XX and

           A3: y in XX;

          consider y1 be set, y2 be Point of M such that

           A4: y = [y1, y2] and y1 in X & y2 <> a or y1 = X & y2 = a by A3, Th37;

          consider x1 be set, x2 be Point of M such that

           A5: x = [x1, x2] and x1 in X & x2 <> a or x1 = X & x2 = a by A2, Th37;

          per cases ;

            suppose

             A6: x1 = y1;

            take d = ( dist (x2,y2));

            thus d in REAL by XREAL_0:def 1;

            let x9,y9 be Element of XX such that

             A7: x9 = x and

             A8: y9 = y;

            let x19,y19 be object, x29,y29 be Point of M such that

             A9: x9 = [x19, x29] and

             A10: y9 = [y19, y29];



             A11: x29 = x2 by A5, A7, A9, XTUPLE_0: 1;

            x19 = x1 by A5, A7, A9, XTUPLE_0: 1;

            hence (x19 = y19 implies d = ( dist (x29,y29))) & (x19 <> y19 implies d = (( dist (x29,a)) + ( dist (a,y29)))) by A4, A6, A8, A10, A11, XTUPLE_0: 1;

          end;

            suppose

             A12: x1 <> y1;

            take d = (( dist (x2,a)) + ( dist (a,y2)));

            thus d in REAL by XREAL_0:def 1;

            let x9,y9 be Element of XX such that

             A13: x9 = x and

             A14: y9 = y;

            let x19,y19 be object, x29,y29 be Point of M such that

             A15: x9 = [x19, x29] and

             A16: y9 = [y19, y29];



             A17: x29 = x2 by A5, A13, A15, XTUPLE_0: 1;

            x19 = x1 by A5, A13, A15, XTUPLE_0: 1;

            hence (x19 = y19 implies d = ( dist (x29,y29))) & (x19 <> y19 implies d = (( dist (x29,a)) + ( dist (a,y29)))) by A4, A12, A14, A16, A17, XTUPLE_0: 1;

          end;

        end;

        consider f be Function of [:XX, XX:], REAL such that

         A18: for x,y be object st x in XX & y in XX holds P[x, y, (f . (x,y))] from BINOP_1:sch 1( A1);

        take f;

        thus thesis by A18;

      end;

      uniqueness

      proof

        set XX = ( [:X, (the carrier of M \ {a}):] \/ { [X, a]});

        let w1,w2 be Function of [:XX, XX:], REAL such that

         A19: for x,y be Element of XX holds for x1,y1 be object, x2,y2 be Point of M st x = [x1, x2] & y = [y1, y2] holds (x1 = y1 implies (w1 . (x,y)) = ( dist (x2,y2))) & (x1 <> y1 implies (w1 . (x,y)) = (( dist (x2,a)) + ( dist (a,y2)))) and

         A20: for x,y be Element of XX holds for x1,y1 be object, x2,y2 be Point of M st x = [x1, x2] & y = [y1, y2] holds (x1 = y1 implies (w2 . (x,y)) = ( dist (x2,y2))) & (x1 <> y1 implies (w2 . (x,y)) = (( dist (x2,a)) + ( dist (a,y2))));

        now

          let x, y such that

           A21: x in XX and

           A22: y in XX;

          consider y1 be set, y2 be Point of M such that

           A23: y = [y1, y2] and y1 in X & y2 <> a or y1 = X & y2 = a by A22, Th37;

          consider x1 be set, x2 be Point of M such that

           A24: x = [x1, x2] and x1 in X & x2 <> a or x1 = X & x2 = a by A21, Th37;

          reconsider x2, y2 as Point of M;

          x1 = y1 or x1 <> y1;

          then (w1 . (x,y)) = ( dist (x2,y2)) & (w2 . (x,y)) = ( dist (x2,y2)) or (w1 . (x,y)) = (( dist (x2,a)) + ( dist (a,y2))) & (w2 . (x,y)) = (( dist (x2,a)) + ( dist (a,y2))) by A19, A20, A21, A22, A24, A23;

          hence (w1 . (x,y)) = (w2 . (x,y));

        end;

        hence thesis by BINOP_1: 1;

      end;

    end

    theorem :: COMPL_SP:39

    for M be MetrStruct, a be Point of M holds for X be non empty set holds (( well_dist (a,X)) is Reflexive implies M is Reflexive) & (( well_dist (a,X)) is symmetric implies M is symmetric) & (( well_dist (a,X)) is triangle Reflexive implies M is triangle) & (( well_dist (a,X)) is discerning Reflexive implies M is discerning)

    proof

      let M be MetrStruct, A be Point of M;

      let X be non empty set;

      consider x0 be object such that

       A1: x0 in X by XBOOLE_0:def 1;

      set w = ( well_dist (A,X));

      set XX = ( [:X, (the carrier of M \ {A}):] \/ { [X, A]});

      thus

       A2: w is Reflexive implies M is Reflexive

      proof

        assume

         A3: w is Reflexive;

        now

          let a be Element of M;

          now

            per cases ;

              suppose a = A;

              then

               A4: [X, a] in XX by Th37;



              hence ( dist (a,a)) = (w . ( [X, a], [X, a])) by Def10

              .= 0 by A3, A4;

            end;

              suppose a <> A;

              then

               A5: [x0, a] in XX by A1, Th37;



              hence ( dist (a,a)) = (w . ( [x0, a], [x0, a])) by Def10

              .= 0 by A3, A5;

            end;

          end;

          hence ( dist (a,a)) = 0 ;

        end;

        hence thesis by METRIC_1: 1;

      end;

      thus w is symmetric implies M is symmetric

      proof

        assume

         A6: w is symmetric;

        now

          let a,b be Element of M;

          now

            per cases ;

              suppose a = A & b = A;

              hence ( dist (a,b)) = ( dist (b,a));

            end;

              suppose

               A7: a = A & b <> A;

              then

               A8: [x0, b] in XX by A1, Th37;



               A9: [X, A] in XX by Th37;

              reconsider xx = x0 as set by TARSKI: 1;

               not xx in xx;

              then

               A10: X <> x0 by A1;



              then (( dist (A,A)) + ( dist (A,b))) = (w . ( [X, A], [x0, b])) by A9, A8, Def10

              .= (w . ( [x0, b], [X, A])) by A6, A9, A8

              .= (( dist (b,A)) + ( dist (A,A))) by A9, A8, A10, Def10;

              hence ( dist (a,b)) = ( dist (b,a)) by A7;

            end;

              suppose

               A11: a <> A & b = A;

              then

               A12: [x0, a] in XX by A1, Th37;



               A13: [X, A] in XX by Th37;

              reconsider xx = x0 as set by TARSKI: 1;

               not xx in xx;

              then

               A14: X <> x0 by A1;



              then (( dist (A,A)) + ( dist (A,a))) = (w . ( [X, A], [x0, a])) by A13, A12, Def10

              .= (w . ( [x0, a], [X, A])) by A6, A13, A12

              .= (( dist (a,A)) + ( dist (A,A))) by A13, A12, A14, Def10;

              hence ( dist (a,b)) = ( dist (b,a)) by A11;

            end;

              suppose

               A15: a <> A & b <> A;

              then

               A16: [x0, b] in XX by A1, Th37;



               A17: [x0, a] in XX by A1, A15, Th37;



              hence ( dist (a,b)) = (w . ( [x0, a], [x0, b])) by A16, Def10

              .= (w . ( [x0, b], [x0, a])) by A6, A17, A16

              .= ( dist (b,a)) by A17, A16, Def10;

            end;

          end;

          hence ( dist (a,b)) = ( dist (b,a));

        end;

        hence thesis by METRIC_1: 3;

      end;

      thus w is triangle Reflexive implies M is triangle

      proof

        assume

         A18: w is triangle Reflexive;

        now

          let a,b,c be Point of M;

          now

            per cases ;

              suppose a = A & b = A & c = A;

              then

              reconsider Xa = [X, a], Xb = [X, b], Xc = [X, c] as Element of XX by Th37;



               A19: ( dist (a,c)) = (w . (Xa,Xc)) by Def10;



               A20: ( dist (a,b)) = (w . (Xa,Xb)) by Def10;

              (w . (Xa,Xc)) <= ((w . (Xa,Xb)) + (w . (Xb,Xc))) by A18;

              hence ( dist (a,c)) <= (( dist (a,b)) + ( dist (b,c))) by A19, A20, Def10;

            end;

              suppose

               A21: a = A & b = A & c <> A;

              ( dist (a,a)) = 0 by A2, A18, METRIC_1: 1;

              hence ( dist (a,c)) <= (( dist (a,b)) + ( dist (b,c))) by A21;

            end;

              suppose

               A22: a = A & b <> A & c = A;

              then

              reconsider Xa = [X, a], Xb = [x0, b], Xc = [X, c] as Element of XX by A1, Th37;

              reconsider xx = x0 as set by TARSKI: 1;

               not xx in xx;

              then

               A23: x0 <> X by A1;

              then

               A24: (( dist (b,c)) + ( dist (a,a))) = (w . (Xb,Xc)) by A22, Def10;



               A25: ( dist (a,a)) = 0 by A2, A18, METRIC_1: 1;



               A26: (w . (Xa,Xc)) <= ((w . (Xa,Xb)) + (w . (Xb,Xc))) by A18;

              (( dist (a,a)) + ( dist (a,b))) = (w . (Xa,Xb)) by A22, A23, Def10;

              hence ( dist (a,c)) <= (( dist (a,b)) + ( dist (b,c))) by A26, A24, A25, Def10;

            end;

              suppose

               A27: a = A & b <> A & c <> A;

              then

              reconsider Xa = [X, a], Xb = [x0, b], Xc = [x0, c] as Element of XX by A1, Th37;

              reconsider xx = x0 as set by TARSKI: 1;

               not xx in xx;

              then

               A28: x0 <> X by A1;

              then

               A29: (( dist (a,a)) + ( dist (a,b))) = (w . (Xa,Xb)) by A27, Def10;



               A30: ( dist (a,a)) = 0 by A2, A18, METRIC_1: 1;



               A31: (w . (Xa,Xc)) <= ((w . (Xa,Xb)) + (w . (Xb,Xc))) by A18;

              (( dist (a,a)) + ( dist (a,c))) = (w . (Xa,Xc)) by A27, A28, Def10;

              hence ( dist (a,c)) <= (( dist (a,b)) + ( dist (b,c))) by A31, A29, A30, Def10;

            end;

              suppose

               A32: a <> A & b = A & c = A;

              ( dist (c,c)) = 0 by A2, A18, METRIC_1: 1;

              hence ( dist (a,c)) <= (( dist (a,b)) + ( dist (b,c))) by A32;

            end;

              suppose

               A33: a <> A & b = A & c <> A;

              then

              reconsider Xa = [x0, a], Xb = [X, b], Xc = [x0, c] as Element of XX by A1, Th37;

              reconsider xx = x0 as set by TARSKI: 1;

               not xx in xx;

              then

               A34: x0 <> X by A1;

              then

               A35: (( dist (b,b)) + ( dist (b,c))) = (w . (Xb,Xc)) by A33, Def10;



               A36: ( dist (b,b)) = 0 by A2, A18, METRIC_1: 1;



               A37: (w . (Xa,Xc)) <= ((w . (Xa,Xb)) + (w . (Xb,Xc))) by A18;

              (( dist (a,b)) + ( dist (b,b))) = (w . (Xa,Xb)) by A33, A34, Def10;

              hence ( dist (a,c)) <= (( dist (a,b)) + ( dist (b,c))) by A37, A35, A36, Def10;

            end;

              suppose

               A38: a <> A & b <> A & c = A;

              then

              reconsider Xa = [x0, a], Xb = [x0, b], Xc = [X, c] as Element of XX by A1, Th37;

              reconsider xx = x0 as set by TARSKI: 1;

               not xx in xx;

              then

               A39: x0 <> X by A1;

              then

               A40: (( dist (b,c)) + ( dist (c,c))) = (w . (Xb,Xc)) by A38, Def10;



               A41: ( dist (c,c)) = 0 by A2, A18, METRIC_1: 1;



               A42: (w . (Xa,Xc)) <= ((w . (Xa,Xb)) + (w . (Xb,Xc))) by A18;

              (( dist (a,c)) + ( dist (c,c))) = (w . (Xa,Xc)) by A38, A39, Def10;

              hence ( dist (a,c)) <= (( dist (a,b)) + ( dist (b,c))) by A42, A40, A41, Def10;

            end;

              suppose a <> A & b <> A & c <> A;

              then

              reconsider Xa = [x0, a], Xb = [x0, b], Xc = [x0, c] as Element of XX by A1, Th37;



               A43: ( dist (a,c)) = (w . (Xa,Xc)) by Def10;



               A44: ( dist (a,b)) = (w . (Xa,Xb)) by Def10;

              (w . (Xa,Xc)) <= ((w . (Xa,Xb)) + (w . (Xb,Xc))) by A18;

              hence ( dist (a,c)) <= (( dist (a,b)) + ( dist (b,c))) by A43, A44, Def10;

            end;

          end;

          hence ( dist (a,c)) <= (( dist (a,b)) + ( dist (b,c)));

        end;

        hence thesis by METRIC_1: 4;

      end;

      assume

       A45: w is discerning Reflexive;

      now

        let a,b be Point of M;

        assume

         A46: ( dist (a,b)) = 0 ;

        now

          per cases ;

            suppose a = A & b = A;

            hence a = b;

          end;

            suppose

             A47: a = A & b <> A;

            then

            reconsider Xa = [X, a], Xb = [x0, b] as Element of XX by A1, Th37;

            reconsider xx = x0 as set by TARSKI: 1;

             not xx in xx;

            then x0 <> X by A1;

            then

             A48: (( dist (a,a)) + ( dist (a,b))) = (w . (Xa,Xb)) by A47, Def10;

            ( dist (a,a)) = 0 by A2, A45, METRIC_1: 1;

            then Xa = Xb by A45, A46, A48;

            hence a = b by XTUPLE_0: 1;

          end;

            suppose

             A49: a <> A & b = A;

            then

            reconsider Xa = [x0, a], Xb = [X, b] as Element of XX by A1, Th37;

            reconsider xx = x0 as set by TARSKI: 1;

             not xx in xx;

            then x0 <> X by A1;

            then

             A50: (( dist (a,b)) + ( dist (b,b))) = (w . (Xa,Xb)) by A49, Def10;

            ( dist (b,b)) = 0 by A2, A45, METRIC_1: 1;

            then Xa = Xb by A45, A46, A50;

            hence a = b by XTUPLE_0: 1;

          end;

            suppose a <> A & b <> A;

            then

            reconsider Xa = [x0, a], Xb = [x0, b] as Element of XX by A1, Th37;

            ( dist (a,b)) = (w . (Xa,Xb)) by Def10;

            then Xa = Xb by A45, A46;

            hence a = b by XTUPLE_0: 1;

          end;

        end;

        hence a = b;

      end;

      hence thesis by METRIC_1: 2;

    end;

    definition

      let M be MetrStruct;

      let a be Point of M;

      let X be set;

      :: COMPL_SP:def11

      func WellSpace (a,X) -> strict MetrStruct equals MetrStruct (# ( [:X, (the carrier of M \ {a}):] \/ { [X, a]}), ( well_dist (a,X)) #);

      coherence ;

    end

    registration

      let M be MetrStruct;

      let a be Point of M;

      let X be set;

      cluster ( WellSpace (a,X)) -> non empty;

      coherence ;

    end



     Lm8: for M be MetrStruct, a be Point of M, X holds (M is Reflexive implies ( WellSpace (a,X)) is Reflexive) & (M is symmetric implies ( WellSpace (a,X)) is symmetric) & (M is triangle symmetric Reflexive implies ( WellSpace (a,X)) is triangle) & (M is triangle symmetric Reflexive discerning implies ( WellSpace (a,X)) is discerning)

    proof

      let M be MetrStruct, a be Point of M, X;

      set XX = ( [:X, (the carrier of M \ {a}):] \/ { [X, a]});

      set w = ( well_dist (a,X));

      set W = ( WellSpace (a,X));

      thus M is Reflexive implies W is Reflexive

      proof

        assume

         A1: M is Reflexive;

        now

          let A be Element of XX;

          consider y be set, b be Point of M such that

           A2: A = [y, b] and y in X & b <> a or y = X & b = a by Th37;



          thus (w . (A,A)) = ( dist (b,b)) by A2, Def10

          .= 0 by A1, METRIC_1: 1;

        end;

        then w is Reflexive;

        hence thesis;

      end;

      thus M is symmetric implies W is symmetric

      proof

        assume M is symmetric;

        then

        reconsider M as symmetric MetrStruct;

        reconsider a as Point of M;

        now

          let A,B be Element of XX;

          consider y1 be set, b1 be Point of M such that

           A3: A = [y1, b1] and

           A4: y1 in X & b1 <> a or y1 = X & b1 = a by Th37;

          consider y2 be set, b2 be Point of M such that

           A5: B = [y2, b2] and

           A6: y2 in X & b2 <> a or y2 = X & b2 = a by Th37;

          now

            per cases by A4, A6;

              suppose b1 = a & y1 = X & b2 = a & y2 = X;

              hence (w . (A,B)) = (w . (B,A)) by A3, A5;

            end;

              suppose

               A7: y1 <> y2;



              hence (w . (A,B)) = (( dist (b1,a)) + ( dist (a,b2))) by A3, A5, Def10

              .= (( dist (a,b1)) + ( dist (a,b2)))

              .= (( dist (a,b1)) + ( dist (b2,a)))

              .= (w . (B,A)) by A3, A5, A7, Def10;

            end;

              suppose

               A8: b1 <> a & b2 <> a & y1 = y2;



              hence (w . (A,B)) = ( dist (b1,b2)) by A3, A5, Def10

              .= ( dist (b2,b1))

              .= (w . (B,A)) by A3, A5, A8, Def10;

            end;

          end;

          hence (w . (A,B)) = (w . (B,A));

        end;

        then w is symmetric;

        hence thesis;

      end;

      thus M is triangle symmetric Reflexive implies ( WellSpace (a,X)) is triangle

      proof

        assume

         A9: M is triangle symmetric Reflexive;

        now

          let A,B,C be Element of XX;

          consider y1 be set, b1 be Point of M such that

           A10: A = [y1, b1] and y1 in X & b1 <> a or y1 = X & b1 = a by Th37;

          consider y2 be set, b2 be Point of M such that

           A11: B = [y2, b2] and y2 in X & b2 <> a or y2 = X & b2 = a by Th37;

          consider y3 be set, b3 be Point of M such that

           A12: C = [y3, b3] and y3 in X & b3 <> a or y3 = X & b3 = a by Th37;

          now

            per cases ;

              suppose

               A13: y1 = y2 & y1 = y3;

              then

               A14: ( dist (b2,b3)) = (w . (B,C)) by A11, A12, Def10;



               A15: ( dist (b1,b2)) = (w . (A,B)) by A10, A11, A13, Def10;

              ( dist (b1,b3)) = (w . (A,C)) by A10, A12, A13, Def10;

              hence (w . (A,C)) <= ((w . (A,B)) + (w . (B,C))) by A9, A15, A14, METRIC_1: 4;

            end;

              suppose

               A16: y1 <> y2 & y1 = y3;

              then

               A17: (( dist (b2,a)) + ( dist (a,b3))) = (w . (B,C)) by A11, A12, Def10;



               A18: ( dist (b1,b2)) <= (( dist (b1,a)) + ( dist (a,b2))) by A9, METRIC_1: 4;



               A19: ( dist (b2,b3)) <= (( dist (b2,a)) + ( dist (a,b3))) by A9, METRIC_1: 4;

              (( dist (b1,a)) + ( dist (a,b2))) = (w . (A,B)) by A10, A11, A16, Def10;

              then

               A20: (( dist (b1,b2)) + ( dist (b2,b3))) <= ((w . (A,B)) + (w . (B,C))) by A17, A18, A19, XREAL_1: 7;



               A21: ( dist (b1,b3)) <= (( dist (b1,b2)) + ( dist (b2,b3))) by A9, METRIC_1: 4;

              ( dist (b1,b3)) = (w . (A,C)) by A10, A12, A16, Def10;

              hence (w . (A,C)) <= ((w . (A,B)) + (w . (B,C))) by A20, A21, XXREAL_0: 2;

            end;

              suppose

               A22: y1 = y2 & y1 <> y3;



               A23: ( dist (b1,a)) <= (( dist (b1,b2)) + ( dist (b2,a))) by A9, METRIC_1: 4;

              (( dist (b1,a)) + ( dist (a,b3))) = (w . (A,C)) by A10, A12, A22, Def10;

              then

               A24: (w . (A,C)) <= ((( dist (b1,b2)) + ( dist (b2,a))) + ( dist (a,b3))) by A23, XREAL_1: 6;



               A25: (( dist (b2,a)) + ( dist (a,b3))) = (w . (B,C)) by A11, A12, A22, Def10;

              ( dist (b1,b2)) = (w . (A,B)) by A10, A11, A22, Def10;

              hence (w . (A,C)) <= ((w . (A,B)) + (w . (B,C))) by A25, A24;

            end;

              suppose

               A26: y1 <> y2 & y1 <> y3 & y2 <> y3;



               A27: 0 <= ( dist (b2,a)) by A9, METRIC_1: 5;

              (( dist (b2,a)) + ( dist (a,b3))) = (w . (B,C)) by A11, A12, A26, Def10;

              then

               A28: ( 0 + ( dist (a,b3))) <= (w . (B,C)) by A27, XREAL_1: 6;



               A29: 0 <= ( dist (a,b2)) by A9, METRIC_1: 5;

              (( dist (b1,a)) + ( dist (a,b2))) = (w . (A,B)) by A10, A11, A26, Def10;

              then

               A30: (( dist (b1,a)) + 0 ) <= (w . (A,B)) by A29, XREAL_1: 6;

              (( dist (b1,a)) + ( dist (a,b3))) = (w . (A,C)) by A10, A12, A26, Def10;

              hence (w . (A,C)) <= ((w . (A,B)) + (w . (B,C))) by A30, A28, XREAL_1: 7;

            end;

              suppose

               A31: y1 <> y2 & y1 <> y3 & y2 = y3;



               A32: ( dist (a,b3)) <= (( dist (a,b2)) + ( dist (b2,b3))) by A9, METRIC_1: 4;

              (( dist (b1,a)) + ( dist (a,b3))) = (w . (A,C)) by A10, A12, A31, Def10;

              then

               A33: (w . (A,C)) <= (( dist (b1,a)) + (( dist (a,b2)) + ( dist (b2,b3)))) by A32, XREAL_1: 7;



               A34: ( dist (b2,b3)) = (w . (B,C)) by A11, A12, A31, Def10;

              (( dist (b1,a)) + ( dist (a,b2))) = (w . (A,B)) by A10, A11, A31, Def10;

              hence (w . (A,C)) <= ((w . (A,B)) + (w . (B,C))) by A34, A33;

            end;

          end;

          hence (w . (A,C)) <= ((w . (A,B)) + (w . (B,C)));

        end;

        then w is triangle;

        hence thesis;

      end;

      assume

       A35: M is triangle symmetric Reflexive discerning;

      now

        let A,B be Element of XX;

        consider y1 be set, b1 be Point of M such that

         A36: A = [y1, b1] and

         A37: y1 in X & b1 <> a or y1 = X & b1 = a by Th37;

        consider y2 be set, b2 be Point of M such that

         A38: B = [y2, b2] and

         A39: y2 in X & b2 <> a or y2 = X & b2 = a by Th37;

        assume

         A40: (w . (A,B)) = 0 ;

        now

          per cases ;

            suppose

             A41: y1 = y2;

            then (w . (A,B)) = ( dist (b1,b2)) by A36, A38, Def10;

            hence A = B by A35, A40, A36, A38, A41, METRIC_1: 2;

          end;

            suppose y1 <> y2;

            then

             A42: (w . (A,B)) = (( dist (b1,a)) + ( dist (a,b2))) by A36, A38, Def10;



             A43: ( dist (b1,a)) >= 0 by A35, METRIC_1: 5;

            ( dist (a,b2)) >= 0 by A35, METRIC_1: 5;

            then ( dist (b1,a)) = 0 by A40, A42, A43;

            hence A = B by A35, A40, A36, A37, A38, A39, A42, METRIC_1: 2;

          end;

        end;

        hence A = B;

      end;

      then w is discerning;

      hence thesis;

    end;

    registration

      let M be Reflexive MetrStruct;

      let a be Point of M;

      let X be set;

      cluster ( WellSpace (a,X)) -> Reflexive;

      coherence by Lm8;

    end

    registration

      let M be symmetric MetrStruct;

      let a be Point of M;

      let X be set;

      cluster ( WellSpace (a,X)) -> symmetric;

      coherence by Lm8;

    end

    registration

      let M be symmetric triangle Reflexive MetrStruct;

      let a be Point of M;

      let X be set;

      cluster ( WellSpace (a,X)) -> triangle;

      coherence by Lm8;

    end

    registration

      let M be MetrSpace;

      let a be Point of M;

      let X be set;

      cluster ( WellSpace (a,X)) -> discerning;

      coherence by Lm8;

    end

    theorem :: COMPL_SP:40

    for M be triangle Reflexive non empty MetrStruct holds for a be Point of M holds for X be non empty set holds ( WellSpace (a,X)) is complete implies M is complete

    proof

      let M be triangle Reflexive non empty MetrStruct;

      let a be Point of M;

      let X be non empty set;

      consider x0 be object such that

       A1: x0 in X by XBOOLE_0:def 1;

      set W = ( WellSpace (a,X));

      assume

       A2: ( WellSpace (a,X)) is complete;

      let S be sequence of M such that

       A3: S is Cauchy;

      defpred P[ object, object] means ((S . $1) <> a implies $2 = [x0, (S . $1)]) & ((S . $1) = a implies $2 = [X, (S . $1)]);



       A4: for x be object st x in NAT holds ex y be object st y in the carrier of W & P[x, y]

      proof

        let x be object;

        assume x in NAT ;

        then

        reconsider i = x as Nat;

        per cases ;

          suppose

           A5: (S . i) <> a;

          take [x0, (S . i)];

          thus thesis by A1, A5, Th37;

        end;

          suppose

           A6: (S . x) = a;

          take [X, a];

          thus thesis by A6, Th37;

        end;

      end;

      consider S9 be sequence of W such that

       A7: for x be object st x in NAT holds P[x, (S9 . x)] from FUNCT_2:sch 1( A4);

      S9 is Cauchy

      proof

        let r;

        assume r > 0 ;

        then

        consider p be Nat such that

         A8: for n,m be Nat st p <= n & p <= m holds ( dist ((S . n),(S . m))) < r by A3;

        take p;

        let n,m be Nat such that

         A9: p <= n and

         A10: p <= m;



         A11: n in NAT & m in NAT by ORDINAL1:def 12;

        per cases ;

          suppose

           A12: (S . n) = a & (S . m) = a;

          then

           A13: [X, (S . m)] = (S9 . m) by A7, A11;

           [X, (S . n)] = (S9 . n) by A7, A12, A11;

          then ( dist ((S9 . n),(S9 . m))) = ( dist ((S . n),(S . m))) by A13, Def10;

          hence thesis by A8, A9, A10;

        end;

          suppose

           A14: (S . n) <> a & (S . m) = a;

          then

           A15: [X, (S . m)] = (S9 . m) by A7, A11;



           A16: ( dist ((S . m),(S . m))) = 0 by METRIC_1: 1;

          reconsider xx = x0 as set by TARSKI: 1;

           not xx in xx;

          then

           A17: X <> x0 by A1;

           [x0, (S . n)] = (S9 . n) by A7, A14, A11;

          then ( dist ((S9 . n),(S9 . m))) = (( dist ((S . n),(S . m))) + ( dist ((S . m),(S . m)))) by A14, A15, A17, Def10;

          hence thesis by A8, A9, A10, A16;

        end;

          suppose

           A18: (S . n) = a & (S . m) <> a;

          then

           A19: [x0, (S . m)] = (S9 . m) by A7, A11;



           A20: ( dist ((S . n),(S . n))) = 0 by METRIC_1: 1;

          reconsider xx = x0 as set by TARSKI: 1;

           not xx in xx;

          then

           A21: X <> x0 by A1;

           [X, (S . n)] = (S9 . n) by A7, A18, A11;

          then ( dist ((S9 . n),(S9 . m))) = (( dist ((S . n),(S . n))) + ( dist ((S . n),(S . m)))) by A18, A19, A21, Def10;

          hence thesis by A8, A9, A10, A20;

        end;

          suppose

           A22: (S . n) <> a & (S . m) <> a;

          then

           A23: [x0, (S . m)] = (S9 . m) by A7, A11;

           [x0, (S . n)] = (S9 . n) by A7, A22, A11;

          then ( dist ((S9 . n),(S9 . m))) = ( dist ((S . n),(S . m))) by A23, Def10;

          hence thesis by A8, A9, A10;

        end;

      end;

      then S9 is convergent by A2;

      then

      consider L be Element of W such that

       A24: for r st r > 0 holds ex n be Nat st for m be Nat st n <= m holds ( dist ((S9 . m),L)) < r;

      consider L1 be set, L2 be Point of M such that

       A25: L = [L1, L2] and L1 in X & L2 <> a or L1 = X & L2 = a by Th37;

      take L2;

      let r;

      assume r > 0 ;

      then

      consider n be Nat such that

       A26: for m be Nat st n <= m holds ( dist ((S9 . m),L)) < r by A24;

      take n;

      let m be Nat such that

       A27: n <= m;



       A28: n in NAT & m in NAT by ORDINAL1:def 12;

      per cases ;

        suppose

         A29: (S . m) = a & L1 = X;

        then (S9 . m) = [X, a] by A7, A28;

        then ( dist ((S9 . m),L)) = ( dist ((S . m),L2)) by A25, A29, Def10;

        hence thesis by A26, A27;

      end;

        suppose

         A30: (S . m) = a & L1 <> X;

        then (S9 . m) = [X, a] by A7, A28;

        then

         A31: ( dist ((S9 . m),L)) = (( dist ((S . m),(S . m))) + ( dist ((S . m),L2))) by A25, A30, Def10;

        ( dist ((S . m),(S . m))) = 0 by METRIC_1: 1;

        hence thesis by A26, A27, A31;

      end;

        suppose

         A32: (S . m) <> a & L1 = x0;

        then (S9 . m) = [x0, (S . m)] by A7, A28;

        then ( dist ((S9 . m),L)) = ( dist ((S . m),L2)) by A25, A32, Def10;

        hence thesis by A26, A27;

      end;

        suppose

         A33: (S . m) <> a & L1 <> x0;

        then (S9 . m) = [x0, (S . m)] by A7, A28;

        then

         A34: ( dist ((S9 . m),L)) = (( dist ((S . m),a)) + ( dist (a,L2))) by A25, A33, Def10;



         A35: (( dist ((S . m),a)) + ( dist (a,L2))) >= ( dist ((S . m),L2)) by METRIC_1: 4;

        ( dist ((S9 . m),L)) < r by A26, A27;

        hence thesis by A34, A35, XXREAL_0: 2;

      end;

    end;

    theorem :: COMPL_SP:41



     Th40: for M be symmetric triangle Reflexive non empty MetrStruct holds for a be Point of M holds for S be sequence of ( WellSpace (a,X)) st S is Cauchy holds (for Xa be Point of ( WellSpace (a,X)) st Xa = [X, a] holds for r st r > 0 holds ex n st for m st m >= n holds ( dist ((S . m),Xa)) < r) or ex n, Y st for m st m >= n holds ex p be Point of M st (S . m) = [Y, p]

    proof

      let M be symmetric triangle Reflexive non empty MetrStruct;

      let a be Point of M;

      set W = ( WellSpace (a,X));

      reconsider Xa = [X, a] as Point of W by Th37;

      let S be sequence of W such that

       A1: S is Cauchy;

      per cases ;

        suppose for r st r > 0 holds ex n st for m st m >= n holds ( dist ((S . m),Xa)) < r;

        hence thesis;

      end;

        suppose ex r st r > 0 & for n holds ex m st m >= n & ( dist ((S . m),Xa)) >= r;

        then

        consider r be Real such that

         A2: r > 0 and

         A3: for n holds ex m st m >= n & ( dist ((S . m),Xa)) >= r;

        consider p be Nat such that

         A4: for n,m be Nat st n >= p & m >= p holds ( dist ((S . n),(S . m))) < r by A1, A2;

        consider p9 be Nat such that

         A5: p9 >= p and

         A6: ( dist ((S . p9),Xa)) >= r by A3;

        consider Y be set, y be Point of M such that

         A7: (S . p9) = [Y, y] and Y in X & y <> a or Y = X & y = a by Th37;

        ex n, Y st for m st m >= n holds ex p be Point of M st (S . m) = [Y, p]

        proof

          take p9, Y;

          let m such that

           A8: m >= p9;

          consider Z be set, z be Point of M such that

           A9: (S . m) = [Z, z] and Z in X & z <> a or Z = X & z = a by Th37;

          Y = Z

          proof



             A10: ( dist (a,z)) >= 0 by METRIC_1: 5;



             A11: ( dist (a,a)) = 0 by METRIC_1: 1;

            X = Y or X <> Y;

            then ( dist ((S . p9),Xa)) = ( dist (y,a)) or ( dist ((S . p9),Xa)) = (( dist (y,a)) + 0 ) by A7, A11, Def10;

            then

             A12: (( dist (y,a)) + ( dist (a,z))) >= (r + 0 ) by A6, A10, XREAL_1: 7;

            assume Y <> Z;

            then

             A13: ( dist ((S . p9),(S . m))) >= r by A7, A9, A12, Def10;

            m >= p by A5, A8, XXREAL_0: 2;

            hence thesis by A4, A5, A13;

          end;

          hence thesis by A9;

        end;

        hence thesis;

      end;

    end;

    theorem :: COMPL_SP:42



     Th41: for M be symmetric triangle Reflexive non empty MetrStruct holds for a be Point of M holds M is complete implies ( WellSpace (a,X)) is complete

    proof

      let M be symmetric triangle Reflexive non empty MetrStruct;

      let a be Point of M;

      set W = ( WellSpace (a,X));

      reconsider Xa = [X, a] as Point of W by Th37;

      assume

       A1: M is complete;

      let S9 be sequence of W such that

       A2: S9 is Cauchy;

      defpred P[ object, object] means ex x st (S9 . $1) = [x, $2];



       A3: for x be object st x in NAT holds ex y be object st y in the carrier of M & P[x, y]

      proof

        let x be object;

        assume x in NAT ;

        then

        reconsider i = x as Nat;

        consider s1 be set, s2 be Point of M such that

         A4: (S9 . i) = [s1, s2] and s1 in X & s2 <> a or s1 = X & s2 = a by Th37;

        take s2;

        thus thesis by A4;

      end;

      consider S be sequence of M such that

       A5: for x be object st x in NAT holds P[x, (S . x)] from FUNCT_2:sch 1( A3);

      S is Cauchy

      proof

        let r;

        assume r > 0 ;

        then

        consider p be Nat such that

         A6: for n,m be Nat st p <= n & p <= m holds ( dist ((S9 . n),(S9 . m))) < r by A2;

        take p;

        let n,m be Nat such that

         A7: p <= n and

         A8: p <= m;



         A9: n in NAT & m in NAT by ORDINAL1:def 12;

        consider x such that

         A10: (S9 . n) = [x, (S . n)] by A5, A9;

        consider y such that

         A11: (S9 . m) = [y, (S . m)] by A5, A9;

        per cases ;

          suppose x = y;

          then ( dist ((S9 . n),(S9 . m))) = ( dist ((S . n),(S . m))) by A10, A11, Def10;

          hence thesis by A6, A7, A8;

        end;

          suppose

           A12: x <> y;



           A13: ( dist ((S . n),(S . m))) <= (( dist ((S . n),a)) + ( dist (a,(S . m)))) by METRIC_1: 4;



           A14: ( dist ((S9 . n),(S9 . m))) < r by A6, A7, A8;

          ( dist ((S9 . n),(S9 . m))) = (( dist ((S . n),a)) + ( dist (a,(S . m)))) by A10, A11, A12, Def10;

          hence thesis by A13, A14, XXREAL_0: 2;

        end;

      end;

      then S is convergent by A1;

      then

      consider L be Element of M such that

       A15: for r st r > 0 holds ex n be Nat st for m be Nat st n <= m holds ( dist ((S . m),L)) < r;

      per cases by A2, Th40;

        suppose

         A16: L = a;

        take Xa;



         A17: ( dist (a,a)) = 0 by METRIC_1: 1;

        let r;

        assume r > 0 ;

        then

        consider n be Nat such that

         A18: for m be Nat st n <= m holds ( dist ((S . m),L)) < r by A15;

        take n;

        let m be Nat such that

         A19: m >= n;



         A20: n in NAT & m in NAT by ORDINAL1:def 12;

        consider x such that

         A21: (S9 . m) = [x, (S . m)] by A5, A20;

        x = X or x <> X;

        then ( dist ((S9 . m),Xa)) = ( dist ((S . m),L)) or ( dist ((S9 . m),Xa)) = (( dist ((S . m),L)) + 0 ) by A16, A21, A17, Def10;

        hence ( dist ((S9 . m),Xa)) < r by A18, A19;

      end;

        suppose

         A22: for Xa be Point of W st Xa = [X, a] holds for r st r > 0 holds ex n st for m st m >= n holds ( dist ((S9 . m),Xa)) < r;

        take Xa;

        let r;

        assume r > 0 ;

        then

        consider n such that

         A23: for m st m >= n holds ( dist ((S9 . m),Xa)) < r by A22;

        reconsider n as Nat;

        take n;

        let m be Nat;

        assume m >= n;

        hence ( dist ((S9 . m),Xa)) < r by A23;

      end;

        suppose

         A24: a <> L & ex n, Y st for m st m >= n holds ex p be Point of M st (S9 . m) = [Y, p];

        then

        consider n, Y such that

         A25: for m st m >= n holds ex p be Point of M st (S9 . m) = [Y, p];



         A26: ex s3 be Point of M st (S9 . n) = [Y, s3] by A25;



         A27: ex s1 be set, s2 be Point of M st (S9 . n) = [s1, s2] & (s1 in X & s2 <> a or s1 = X & s2 = a) by Th37;

        per cases by A27, A26, XTUPLE_0: 1;

          suppose Y in X;

          then

          reconsider YL = [Y, L] as Point of W by A24, Th37;

          take YL;

          let r;

          assume r > 0 ;

          then

          consider p be Nat such that

           A28: for m be Nat st p <= m holds ( dist ((S . m),L)) < r by A15;

          reconsider mm = ( max (p,n)) as Nat by TARSKI: 1;

          take mm;

          let m be Nat such that

           A29: m >= mm;



           A30: n in NAT & m in NAT by ORDINAL1:def 12;

          consider x such that

           A31: (S9 . m) = [x, (S . m)] by A5, A30;

          mm >= n by XXREAL_0: 25;

          then ex pm be Point of M st (S9 . m) = [Y, pm] by A25, A29, XXREAL_0: 2;

          then x = Y by A31, XTUPLE_0: 1;

          then

           A32: ( dist ((S9 . m),YL)) = ( dist ((S . m),L)) by A31, Def10;

          mm >= p by XXREAL_0: 25;

          then m >= p by A29, XXREAL_0: 2;

          hence ( dist ((S9 . m),YL)) < r by A28, A32;

        end;

          suppose

           A33: Y = X;

          reconsider n as Nat;

          take Xa;

          let r such that

           A34: r > 0 ;

          take n;

          let m be Nat;

          assume m >= n;

          then

           A35: ex t3 be Point of M st (S9 . m) = [Y, t3] by A25;

          consider t1 be set, t2 be Point of M such that

           A36: (S9 . m) = [t1, t2] and

           A37: t1 in X & t2 <> a or t1 = X & t2 = a by Th37;

          Y = t1 by A36, A35, XTUPLE_0: 1;

          hence ( dist ((S9 . m),Xa)) < r by A33, A34, A36, A37, METRIC_1: 1;

        end;

      end;

    end;

    theorem :: COMPL_SP:43



     Th42: for M be symmetric triangle Reflexive non empty MetrStruct st M is complete holds for a be Point of M st ex b be Point of M st ( dist (a,b)) <> 0 holds for X be infinite set holds ( WellSpace (a,X)) is complete & ex S be non-empty pointwise_bounded SetSequence of ( WellSpace (a,X)) st S is closed & S is non-ascending & ( meet S) is empty

    proof

      let M be symmetric triangle Reflexive non empty MetrStruct such that

       A1: M is complete;

      let a be Point of M;

      assume ex b be Point of M st ( dist (a,b)) <> 0 ;

      then

      consider b be Point of M such that

       A2: ( dist (a,b)) <> 0 ;

      let X be infinite set;

      set W = ( WellSpace (a,X));

      thus W is complete by A1, Th41;

      set TW = ( TopSpaceMetr W);

      consider f be sequence of X such that

       A3: f is one-to-one by DICKSON: 3;

      defpred p[ object, object] means $2 = [(f . $1), b];



       A4: b <> a by A2, METRIC_1: 1;



       A5: for x be object st x in NAT holds ex y be object st y in the carrier of TW & p[x, y]

      proof

        let x be object;

        assume x in NAT ;

        then x in ( dom f) by FUNCT_2:def 1;

        then

         A6: (f . x) in ( rng f) by FUNCT_1:def 3;

        take [(f . x), b];

        thus thesis by A4, A6, Th37;

      end;

      consider s be sequence of the carrier of TW such that

       A7: for x be object st x in NAT holds p[x, (s . x)] from FUNCT_2:sch 1( A5);

      deffunc P( object) = {(s . $1)};



       A8: for x be object st x in NAT holds P(x) in ( bool the carrier of TW)

      proof



         A9: ( dom s) = NAT by FUNCT_2:def 1;

        let x be object;

        assume x in NAT ;

        then (s . x) in ( rng s) by A9, FUNCT_1:def 3;

        then P(x) is Subset of W by SUBSET_1: 33;

        hence thesis;

      end;

      consider S be SetSequence of TW such that

       A10: for x be object st x in NAT holds (S . x) = P(x) from FUNCT_2:sch 2( A8);

       A11:

      now

        let x1,x2 be object such that

         A12: x1 in NAT and

         A13: x2 in NAT and

         A14: (S . x1) = (S . x2);



         A15: (S . x2) = {(s . x2)} by A10, A13;



         A16: (s . x1) = [(f . x1), b] by A7, A12;



         A17: (s . x1) in {(s . x1)} by TARSKI:def 1;



         A18: (s . x2) = [(f . x2), b] by A7, A13;

        (S . x1) = {(s . x1)} by A10, A12;

        then (s . x1) = (s . x2) by A14, A15, A17, TARSKI:def 1;

        then (f . x1) = (f . x2) by A16, A18, XTUPLE_0: 1;

        hence x1 = x2 by A3, A12, A13, FUNCT_2: 19;

      end;

      reconsider rngs = ( rng s) as Subset of TW;

      set F = { {x} where x be Element of TW : x in rngs };

      reconsider F as Subset-Family of TW by RELSET_2: 16;

      ( dist (a,b)) > 0 by A2, METRIC_1: 5;

      then

       A19: (2 * ( dist (a,b))) > 0 by XREAL_1: 129;



       A20: ( rng S) c= F

      proof

        let x be object;

        assume x in ( rng S);

        then

        consider y be object such that

         A21: y in ( dom S) and

         A22: (S . y) = x by FUNCT_1:def 3;

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

        then

         A23: (s . y) in rngs by A21, FUNCT_1:def 3;

        x = {(s . y)} by A10, A21, A22;

        hence thesis by A23;

      end;

      now

        let x be object;

        assume x in ( dom S);

        then (S . x) = {(s . x)} by A10;

        hence (S . x) is non empty;

      end;

      then S is non-empty by FUNCT_1:def 9;

      then

      consider R be non-empty closed SetSequence of TW such that

       A24: R is non-ascending and

       A25: F is locally_finite & S is one-to-one implies ( meet R) = {} and

       A26: for i holds ex Si be Subset-Family of TW st (R . i) = ( Cl ( union Si)) & Si = { (S . j) where j be Element of NAT : j >= i } by A20, Th23;

      reconsider R9 = R as non-empty SetSequence of W;

       A27:

      now

        let x,y be Point of W such that

         A28: x in rngs and

         A29: y in rngs and

         A30: x <> y;

        consider y1 be object such that

         A31: y1 in ( dom s) and

         A32: (s . y1) = y by A29, FUNCT_1:def 3;



         A33: y = [(f . y1), b] by A7, A31, A32;

        consider x1 be object such that

         A34: x1 in ( dom s) and

         A35: (s . x1) = x by A28, FUNCT_1:def 3;

        x = [(f . x1), b] by A7, A34, A35;

        then (( well_dist (a,X)) . (x,y)) = (( dist (b,a)) + ( dist (a,b))) by A30, A33, Def10;

        hence ( dist (x,y)) = (2 * ( dist (a,b)));

      end;

      now

        let i;

        consider Si be Subset-Family of TW such that

         A36: (R . i) = ( Cl ( union Si)) and

         A37: Si = { (S . j) where j be Element of NAT : j >= i } by A26;

        reconsider SI = ( union Si) as Subset of W;

        now

          let x,y be Point of W such that

           A38: x in SI and

           A39: y in SI;

          consider xS be set such that

           A40: x in xS and

           A41: xS in Si by A38, TARSKI:def 4;

          consider j1 be Element of NAT such that

           A42: xS = (S . j1) and j1 >= i by A37, A41;



           A43: (S . j1) = {(s . j1)} by A10;



           A44: ( dom s) = NAT by FUNCT_2:def 1;

          then (s . j1) in rngs by FUNCT_1:def 3;

          then

           A45: x in rngs by A40, A42, A43, TARSKI:def 1;

          consider yS be set such that

           A46: y in yS and

           A47: yS in Si by A39, TARSKI:def 4;

          consider j2 be Element of NAT such that

           A48: yS = (S . j2) and j2 >= i by A37, A47;



           A49: (S . j2) = {(s . j2)} by A10;

          (s . j2) in rngs by A44, FUNCT_1:def 3;

          then

           A50: y in rngs by A46, A48, A49, TARSKI:def 1;

          x = y or x <> y;

          hence ( dist (x,y)) <= (2 * ( dist (a,b))) by A19, A27, A45, A50, METRIC_1: 1;

        end;

        then SI is bounded by A19;

        hence (R9 . i) is bounded by A36, Th8;

      end;

      then

      reconsider R9 as non-empty pointwise_bounded SetSequence of W by Def1;

      take R9;

      thus R9 is closed & R9 is non-ascending by A24, Th7;

      for x,y be Point of W st x <> y & x in rngs & y in rngs holds ( dist (x,y)) >= (2 * ( dist (a,b))) by A27;

      hence thesis by A25, A19, A11, Lm7, FUNCT_2: 19;

    end;

    theorem :: COMPL_SP:44

    ex M be non empty MetrSpace st M is complete & ex S be non-empty pointwise_bounded SetSequence of M st S is closed & S is non-ascending & ( meet S) is empty

    proof

      reconsider D = ( DiscreteSpace 2) as non empty MetrSpace;

       0 in ( Segm 2) & 1 in ( Segm 2) by NAT_1: 44;

      then

      reconsider a = 0 , b = 1 as Point of D;

      ( TopSpaceMetr D) is compact;

      then

       A1: D is complete by TBSP_1: 8;



       A2: 1 = ( dist (a,b)) by METRIC_1:def 10;

      then

       A3: ex S be non-empty pointwise_bounded SetSequence of ( WellSpace (a, NAT )) st S is closed & S is non-ascending & ( meet S) is empty by A1, Th42;

      ( WellSpace (a, NAT )) is complete by A2, A1, Th42;

      hence thesis by A3;

    end;