metrizts.miz



    begin

    reserve T,T1,T2 for TopSpace,

A,B for Subset of T,

F,G for Subset-Family of T,

A1 for Subset of T1,

A2 for Subset of T2,

TM,TM1,TM2 for metrizable TopSpace,

Am,Bm for Subset of TM,

Fm,Gm for Subset-Family of TM,

C for Cardinal,

iC for infinite Cardinal;

    definition

      let T1, T2, A1, A2;

      :: METRIZTS:def1

      pred A1,A2 are_homeomorphic means ((T1 | A1),(T2 | A2)) are_homeomorphic ;

    end

    

     Lm1: for T1,T2 be empty TopSpace holds (T1,T2) are_homeomorphic

    proof

      let T1,T2 be empty TopSpace;

      reconsider E = {} as Function of T1, T2 by FUNCT_2: 1, RELAT_1: 38;

      

       A1: (E " ) is continuous;

      E is continuous;

      then E is being_homeomorphism by A1;

      hence thesis by T_0TOPSP:def 1;

    end;

    theorem :: METRIZTS:1

    (T1,T2) are_homeomorphic iff (( [#] T1),( [#] T2)) are_homeomorphic

    proof

      

       A1: (T1 | ( [#] T1)) = the TopStruct of T1 & (T2 | ( [#] T2)) = the TopStruct of T2 by TSEP_1: 93;

      per cases ;

        suppose

         A2: T2 is non empty;

        thus (T1,T2) are_homeomorphic implies (( [#] T1),( [#] T2)) are_homeomorphic by A1, A2, TOPREALA: 15;

        assume (( [#] T1),( [#] T2)) are_homeomorphic ;

        then ( the TopStruct of T1, the TopStruct of T2) are_homeomorphic by A1;

        hence thesis by A2, TOPREALA: 15;

      end;

        suppose

         A3: T2 is empty;

        hereby

          assume (T1,T2) are_homeomorphic ;

          then T1 is empty iff T2 is empty by YELLOW14: 18;

          then ((T1 | ( [#] T1)),(T2 | ( [#] T2))) are_homeomorphic by A3, Lm1;

          hence (( [#] T1),( [#] T2)) are_homeomorphic ;

        end;

        assume (( [#] T1),( [#] T2)) are_homeomorphic ;

        then ((T1 | ( [#] T1)),(T2 | ( [#] T2))) are_homeomorphic ;

        then T1 is empty by A3, YELLOW14: 18;

        hence thesis by A3, Lm1;

      end;

    end;

    theorem :: METRIZTS:2

    

     Th2: for f be Function of T1, T2 st f is being_homeomorphism holds for g be Function of (T1 | A1), (T2 | (f .: A1)) st g = (f | A1) holds g is being_homeomorphism

    proof

      let f be Function of T1, T2 such that

       A1: f is being_homeomorphism;

      

       A2: ( dom f) = ( [#] T1) by A1;

      (T1,T2) are_homeomorphic by A1, T_0TOPSP:def 1;

      then T1 is empty iff T2 is empty by YELLOW14: 18;

      then

       A3: ( [#] T1) = {} iff ( [#] T2) = {} ;

      

       A4: ( rng f) = ( [#] T2) by A1;

      set B = (f .: A1);

      let g be Function of (T1 | A1), (T2 | B) such that

       A5: g = (f | A1);

      

       A6: ( rng g) = B by A5, RELAT_1: 115;

      

       A7: f is one-to-one by A1;

      then

       A8: g is one-to-one by A5, FUNCT_1: 52;

      

       A9: ( dom g) = (( dom f) /\ A1) by A5, RELAT_1: 61

      .= A1 by A2, XBOOLE_1: 28;

      set TA = (T1 | A1), TB = (T2 | B);

      

       A10: ( [#] TA) = A1 by PRE_TOPC:def 5;

      

       A11: ( [#] TA) = {} iff ( [#] TB) = {} by A9;

      

       A12: ( [#] TB) = B by PRE_TOPC:def 5;

      

       A13: f is continuous by A1;

      for P be Subset of TB st P is open holds (g " P) is open

      proof

        let P be Subset of TB;

        assume P is open;

        then

        consider P1 be Subset of T2 such that

         A14: P1 is open and

         A15: P = (P1 /\ B) by A12, TSP_1:def 1;

        reconsider PA = ((f " P1) /\ A1) as Subset of TA by A10, XBOOLE_1: 17;

        A1 = (f " B) by A2, A7, FUNCT_1: 94;

        then (A1 /\ PA) = PA & PA = (f " P) by A15, FUNCT_1: 68, XBOOLE_1: 17, XBOOLE_1: 28;

        then

         A16: (g " P) = PA by A5, FUNCT_1: 70;

        (f " P1) is open by A3, A13, A14, TOPS_2: 43;

        hence thesis by A10, A16, TSP_1:def 1;

      end;

      then

       A17: g is continuous by A11, TOPS_2: 43;

      

       A18: (f " ) is continuous by A1;

      for P be Subset of TA st P is open holds ((g " ) " P) is open

      proof

        let P be Subset of TA;

        assume P is open;

        then

        consider P1 be Subset of T1 such that

         A19: P1 is open and

         A20: P = (P1 /\ A1) by A10, TSP_1:def 1;

        reconsider PB = (((f " ) " P1) /\ B) as Subset of TB by A12, XBOOLE_1: 17;

        

         A21: ((f " ) " P1) is open by A3, A18, A19, TOPS_2: 43;

        B = ((f " ) " A1) by A4, A7, TOPS_2: 54;

        

        then PB = ((f " ) " (P1 /\ A1)) by FUNCT_1: 68

        .= (f .: P) by A4, A7, A20, TOPS_2: 54

        .= (g .: P) by A5, A10, RELAT_1: 129

        .= ((g " ) " P) by A6, A8, A12, TOPS_2: 54;

        hence thesis by A12, A21, TSP_1:def 1;

      end;

      then (g " ) is continuous by A11, TOPS_2: 43;

      hence thesis by A6, A9, A10, A8, A12, A17;

    end;

    theorem :: METRIZTS:3

    for f be Function of T1, T2 st f is being_homeomorphism holds (A1,(f .: A1)) are_homeomorphic

    proof

      let f be Function of T1, T2 such that

       A1: f is being_homeomorphism;

      ( dom f) = ( [#] T1) by A1;

      

      then

       A2: ( dom (f | A1)) = (( [#] T1) /\ A1) by RELAT_1: 61

      .= A1 by XBOOLE_1: 28

      .= ( [#] (T1 | A1)) by PRE_TOPC:def 5;

      ( rng (f | A1)) = (f .: A1) by RELAT_1: 115

      .= ( [#] (T2 | (f .: A1))) by PRE_TOPC:def 5;

      then

      reconsider g = (f | A1) as Function of (T1 | A1), (T2 | (f .: A1)) by A2, FUNCT_2: 1;

      g is being_homeomorphism by A1, Th2;

      then ((T1 | A1),(T2 | (f .: A1))) are_homeomorphic by T_0TOPSP:def 1;

      hence thesis;

    end;

    

     Lm2: for T1,T2 be non empty TopSpace st (T1,T2) are_homeomorphic holds ( weight T2) c= ( weight T1)

    proof

      let T1,T2 be non empty TopSpace;

      defpred P[ object] means not contradiction;

      consider B1 be Basis of T1 such that

       A1: ( card B1) = ( weight T1) by WAYBEL23: 74;

      assume (T1,T2) are_homeomorphic ;

      then

      consider f be Function of T1, T2 such that

       A2: f is being_homeomorphism by T_0TOPSP:def 1;

      deffunc F( Subset of T1) = (f .: $1);

      defpred PP[ object] means $1 in B1 & P[$1];

      

       A3: ( card { F(w) where w be Subset of T1 : PP[w] }) c= ( card B1) from BORSUK_2:sch 1;

      consider B2 be Subset-Family of T2 such that

       A4: B2 = { F(w) where w be Subset of T1 : PP[w] } from LMOD_7:sch 5;

      

       A5: for A be Subset of T2 st A is open holds for p be Point of T2 st p in A holds ex a be Subset of T2 st a in B2 & p in a & a c= A

      proof

        let A be Subset of T2;

        assume A is open;

        then

         A6: (f " A) is open by A2, TOPGRP_1: 26;

        let p be Point of T2 such that

         A7: p in A;

        

         A8: ( rng f) = ( [#] T2) by A2;

        then

        consider x be object such that

         A9: x in ( dom f) and

         A10: (f . x) = p by FUNCT_1:def 3;

        

         A11: x in (f " A) by A7, A9, A10, FUNCT_1:def 7;

        reconsider x as Point of T1 by A9;

        consider a1 be Subset of T1 such that

         A12: a1 in B1 & x in a1 and

         A13: a1 c= (f " A) by A6, A11, YELLOW_9: 31;

        take a = F(a1);

        a c= (f .: (f " A)) by A13, RELAT_1: 123;

        hence thesis by A4, A8, A9, A10, A12, FUNCT_1: 77, FUNCT_1:def 6;

      end;

      

       A14: B1 c= the topology of T1 by TOPS_2: 64;

      B2 c= the topology of T2

      proof

        let x be object;

        assume x in B2;

        then

        consider w be Subset of T1 such that

         A15: x = F(w) and

         A16: PP[w] by A4;

        w is open by A14, A16;

        then F(w) is open by A2, TOPGRP_1: 25;

        hence thesis by A15;

      end;

      then

      reconsider B2 as Basis of T2 by A5, YELLOW_9: 32;

      ( weight T2) c= ( card B2) by WAYBEL23: 73;

      hence thesis by A1, A4, A3;

    end;

    

     Lm3: for T be empty TopSpace holds ( weight T) is empty

    proof

      let T be empty TopSpace;

      reconsider B = {} as empty Subset-Family of T by TOPGEN_4: 18;

      B c= the topology of T & 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 B & p in a & a c= A;

      then

      reconsider B as Basis of T by YELLOW_9: 32;

      ( weight T) c= ( card B) by WAYBEL23: 73;

      hence thesis;

    end;

    theorem :: METRIZTS:4

    

     Th4: (T1,T2) are_homeomorphic implies ( weight T1) = ( weight T2)

    proof

      assume

       A1: (T1,T2) are_homeomorphic ;

      per cases ;

        suppose

         A2: ( [#] T1) = {} or ( [#] T2) = {} ;

        

         A3: T1 is empty iff T2 is empty by A1, YELLOW14: 18;

        then ( weight T1) = 0 by A2, Lm3;

        hence thesis by A2, A3, Lm3;

      end;

        suppose T1 is non empty & T2 is non empty;

        then ( weight T2) c= ( weight T1) & ( weight T1) c= ( weight T2) by A1, Lm2;

        hence thesis;

      end;

    end;

    registration

      cluster empty -> metrizable for TopSpace;

      coherence

      proof

        let T be TopSpace;

        set cT = the carrier of T;

        

         A1: ( dom {} ) = {} & ( rng {} ) c= REAL ;

        assume

         A2: T is empty;

        then

         A3: ( bool cT) = { {} } by ZFMISC_1: 1;

        cT = {} by A2;

        then [:cT, cT:] = {} by ZFMISC_1: 90;

        then

        reconsider E = {} as Function of [:cT, cT:], REAL by A1, FUNCT_2: 2;

        set M = ( SpaceMetr (cT,E));

        take E;

        thus E is_metric_of cT

        proof

          let a,b,c be Element of cT;

          

           A4: a = 0 & b = 0 by A2, SUBSET_1:def 1;

          thus (E . (a,b)) = 0 iff a = b by A4;

          thus (E . (a,b)) = (E . (b,a)) by A4;

          (E . (a,b)) = 0 ;

          hence (E . (a,c)) <= ((E . (a,b)) + (E . (b,c)));

        end;

        then

         A5: M = MetrStruct (# cT, E #) by PCOMPS_1:def 7;

        then cT in ( Family_open_set M) by PCOMPS_1: 30;

        then ( Family_open_set M) = { {} } by A3, A5, ZFMISC_1: 33;

        hence thesis by A3, ZFMISC_1: 33;

      end;

      cluster metrizable -> T_4 for TopSpace;

      coherence

      proof

        let T be TopSpace such that

         A6: T is metrizable;

        per cases ;

          suppose

           A7: T is empty;

          then for F1,F2 be Subset of T st F1 is closed & F2 is closed & F1 misses F2 holds ex G1,G2 be Subset of T st G1 is open & G2 is open & F1 c= G1 & F2 c= G2 & G1 misses G2;

          then T is normal;

          hence thesis by A7;

        end;

          suppose T is non empty;

          then

          reconsider t = T as metrizable non empty TopSpace by A6;

          t is regular & ex Bn be FamilySequence of t st Bn is Basis_sigma_locally_finite by NAGATA_2: 19;

          then t is T_1 & T is normal by NAGATA_1: 20, NAGATA_2: 19;

          hence thesis;

        end;

      end;

      let M be MetrSpace;

      cluster ( TopSpaceMetr M) -> metrizable;

      coherence

      proof

        per cases ;

          suppose M is empty;

          then ( TopSpaceMetr M) is empty;

          hence thesis;

        end;

          suppose M is non empty;

          then

          reconsider m = M as non empty MetrSpace;

          set TM = ( TopSpaceMetr M);

          reconsider CM = ( [#] M) as non empty Subset of m;

          reconsider CTM = ( [#] TM) as Subset of TM;

          set TMM = ( TopSpaceMetr (m | CM));

          

           A8: ( [#] (m | CM)) = CM by TOPMETR:def 2;

          then

          reconsider D = the distance of (m | CM) as Function of [:the carrier of TM, the carrier of TM:], REAL ;

          take D;

          

           A9: D is_metric_of the carrier of TM by A8, PCOMPS_1: 35;

          (TM | CTM) = TMM & TM is SubSpace of TM by HAUSDORF: 16, TSEP_1: 2;

          

          then the topology of ( TopSpaceMetr M) = the topology of ( TopSpaceMetr (m | CM)) by A8, TSEP_1: 5

          .= ( Family_open_set ( SpaceMetr (the carrier of TM,D))) by A8, A9, PCOMPS_1:def 7;

          hence thesis by A8, PCOMPS_1: 35;

        end;

      end;

    end

    registration

      let TM, Am;

      cluster (TM | Am) -> metrizable;

      coherence

      proof

        per cases ;

          suppose Am is empty;

          hence thesis;

        end;

          suppose

           A1: Am is non empty;

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

           A2: metr is_metric_of the carrier of TM and

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

          

           A4: TM is non empty by A1;

          then

          reconsider TMM = ( SpaceMetr (the carrier of TM,metr)) as non empty MetrSpace by A2, PCOMPS_1: 36;

          reconsider Atm = Am as non empty Subset of TMM by A1, A2, A4, PCOMPS_2: 4;

          reconsider ATM = Atm as non empty Subset of ( TopSpaceMetr TMM);

          TM is SubSpace of TM & the carrier of ( TopSpaceMetr TMM) = the carrier of TM by A2, A4, PCOMPS_2: 4, TSEP_1: 2;

          then ( TopSpaceMetr TMM) is SubSpace of TM by A3, TMAP_1: 6;

          then

           A5: (( TopSpaceMetr TMM) | ATM) is SubSpace of TM by TSEP_1: 7;

          (( TopSpaceMetr TMM) | ATM) = ( TopSpaceMetr (TMM | Atm)) & ( [#] (( TopSpaceMetr TMM) | ATM)) = ATM by HAUSDORF: 16, PRE_TOPC:def 5;

          hence thesis by A5, PRE_TOPC:def 5;

        end;

      end;

    end

    registration

      let TM1, TM2;

      cluster [:TM1, TM2:] -> metrizable;

      coherence

      proof

        per cases ;

          suppose [:TM1, TM2:] is empty;

          hence thesis;

        end;

          suppose

           A1: [:TM1, TM2:] is non empty;

          then

           A2: TM2 is non empty;

          consider metr2 be Function of [:the carrier of TM2, the carrier of TM2:], REAL such that

           A3: metr2 is_metric_of the carrier of TM2 and

           A4: ( Family_open_set ( SpaceMetr (the carrier of TM2,metr2))) = the topology of TM2 by PCOMPS_1:def 8;

          set tm2 = ( SpaceMetr (the carrier of TM2,metr2));

          consider metr1 be Function of [:the carrier of TM1, the carrier of TM1:], REAL such that

           A5: metr1 is_metric_of the carrier of TM1 and

           A6: ( Family_open_set ( SpaceMetr (the carrier of TM1,metr1))) = the topology of TM1 by PCOMPS_1:def 8;

          set tm1 = ( SpaceMetr (the carrier of TM1,metr1));

          

           A7: TM1 is non empty by A1;

          then

          reconsider tm1, tm2 as non empty MetrStruct by A5, A3, A2, PCOMPS_1: 36;

          

           A8: the TopStruct of TM2 = the TopStruct of ( TopSpaceMetr tm2) by A3, A4, A2, PCOMPS_2: 4;

           the TopStruct of TM1 = the TopStruct of ( TopSpaceMetr tm1) by A7, A5, A6, PCOMPS_2: 4;

          

          then [:TM1, TM2:] = [:( TopSpaceMetr tm1), ( TopSpaceMetr tm2):] by A8, WAYBEL29: 7

          .= ( TopSpaceMetr ( max-Prod2 (tm1,tm2))) by TOPREAL7: 23;

          hence thesis;

        end;

      end;

    end

    registration

      let T be empty TopSpace;

      cluster ( weight T) -> empty;

      coherence by Lm3;

    end

    theorem :: METRIZTS:5

    

     Th5: ( weight [:T1, T2:]) c= (( weight T1) *` ( weight T2))

    proof

      per cases ;

        suppose T1 is empty or T2 is empty;

        hence thesis;

      end;

        suppose

         A1: T1 is non empty & T2 is non empty;

        consider B2 be Basis of T2 such that

         A2: ( card B2) = ( weight T2) by WAYBEL23: 74;

        consider B1 be Basis of T1 such that

         A3: ( card B1) = ( weight T1) by WAYBEL23: 74;

        reconsider B12 = { [:a, b:] where a be Subset of T1, b be Subset of T2 : a in B1 & b in B2 } as Basis of [:T1, T2:] by A1, YELLOW_9: 40;

        reconsider B1, B2, B12 as non empty set by A1, YELLOW12: 34;

        deffunc F( Element of [:B1, B2:]) = [:($1 `1 ), ($1 `2 ):];

        

         A4: for x be Element of [:B1, B2:] holds F(x) is Element of B12

        proof

          let x be Element of [:B1, B2:];

          (x `1 ) in B1 & (x `2 ) in B2;

          then F(x) in B12;

          hence thesis;

        end;

        consider f be Function of [:B1, B2:], B12 such that

         A5: for x be Element of [:B1, B2:] holds (f . x) = F(x) from FUNCT_2:sch 9( A4);

        

         A6: ( dom f) = [:B1, B2:] by FUNCT_2:def 1;

        B12 c= ( rng f)

        proof

          let x be object;

          assume x in B12;

          then

          consider a be Subset of T1, b be Subset of T2 such that

           A7: x = [:a, b:] and

           A8: a in B1 & b in B2;

          reconsider ab = [a, b] as Element of [:B1, B2:] by A8, ZFMISC_1: 87;

          ( [a, b] `1 ) = a & ( [a, b] `2 ) = b;

          then x = (f . ab) by A5, A7;

          hence thesis by A6, FUNCT_1:def 3;

        end;

        then

         A9: ( weight [:T1, T2:]) c= ( card B12) & ( card B12) c= ( card [:B1, B2:]) by A6, CARD_1: 12, WAYBEL23: 73;

        ( card [:B1, B2:]) = ( card [:( card B1), ( card B2):]) by CARD_2: 7

        .= (( card B1) *` ( card B2)) by CARD_2:def 2;

        hence thesis by A3, A2, A9;

      end;

    end;

    theorem :: METRIZTS:6

    

     Th6: T1 is non empty & T2 is non empty implies ( weight T1) c= ( weight [:T1, T2:]) & ( weight T2) c= ( weight [:T1, T2:])

    proof

      defpred P[ object] means not contradiction;

      set PR2 = ( pr2 (the carrier of T1,the carrier of T2));

      set PR1 = ( pr1 (the carrier of T1,the carrier of T2));

      assume T1 is non empty & T2 is non empty;

      then

      reconsider t1 = T1, t2 = T2 as non empty TopSpace;

      reconsider T12 = [:t1, t2:] as non empty TopSpace;

      consider B12 be Basis of T12 such that

       A1: ( card B12) = ( weight T12) by WAYBEL23: 74;

      deffunc F1( Subset of T12) = (PR1 .: $1);

      defpred PP[ object] means $1 in B12 & P[$1];

      consider B1 be Subset-Family of T1 such that

       A2: B1 = { F1(w) where w be Subset of T12 : PP[w] } from LMOD_7:sch 5;

      

       A3: B12 c= the topology of T12 by TOPS_2: 64;

      

       A4: B1 c= the topology of T1

      proof

        let x be object;

        assume x in B1;

        then

        consider w be Subset of T12 such that

         A5: x = F1(w) and

         A6: PP[w] by A2;

        w is open by A3, A6;

        then F1(w) is open by BORSUK_1: 18;

        hence thesis by A5;

      end;

      for A be Subset of T1 st A is open holds for p be Point of T1 st p in A holds ex a be Subset of T1 st a in B1 & p in a & a c= A

      proof

        let A be Subset of T1;

        assume A is open;

        then

         A7: [:A, ( [#] T2):] is open by BORSUK_1: 6;

        set p2 = the Point of T2;

        

         A8: p2 in ( [#] t2);

        let p1 be Point of T1;

        assume p1 in A;

        then

         A9: [p1, p2] in [:A, ( [#] T2):] by A8, ZFMISC_1: 87;

        then

        reconsider p = [p1, p2] as Point of T12;

        consider a12 be Subset of T12 such that

         A10: a12 in B12 and

         A11: p in a12 and

         A12: a12 c= [:A, ( [#] T2):] by A7, A9, YELLOW_9: 31;

        p1 in ( [#] t1) & p2 in ( [#] t2);

        then

         A13: (PR1 . (p1,p2)) = p1 by FUNCT_3:def 4;

        a12 is open by A3, A10;

        then

        reconsider a = F1(a12) as open Subset of T1 by BORSUK_1: 18;

        take a;

        ( dom PR1) = [:( [#] T1), ( [#] T2):] by FUNCT_3:def 4

        .= ( [#] T12) by BORSUK_1:def 2;

        hence a in B1 & p1 in a by A2, A10, A11, A13, FUNCT_1:def 6;

        let y be object;

        assume y in a;

        then

        consider x be object such that

         A14: x in ( dom PR1) and

         A15: x in a12 & y = (PR1 . x) by FUNCT_1:def 6;

        consider x1,x2 be object such that

         A16: x1 in ( [#] T1) & x2 in ( [#] T2) and

         A17: x = [x1, x2] by A14, ZFMISC_1:def 2;

        (PR1 . (x1,x2)) = x1 by A16, FUNCT_3:def 4;

        hence thesis by A12, A15, A17, ZFMISC_1: 87;

      end;

      then

      reconsider B1 as Basis of T1 by A4, YELLOW_9: 32;

      

       A18: ( card { F1(w) where w be Subset of T12 : PP[w] }) c= ( card B12) from BORSUK_2:sch 1;

      ( weight t1) c= ( card B1) by WAYBEL23: 73;

      hence ( weight T1) c= ( weight [:T1, T2:]) by A1, A2, A18;

      deffunc F2( Subset of T12) = (PR2 .: $1);

      consider B2 be Subset-Family of T2 such that

       A19: B2 = { F2(w) where w be Subset of T12 : PP[w] } from LMOD_7:sch 5;

      

       A20: for A be Subset of T2 st A is open holds for p be Point of T2 st p in A holds ex a be Subset of T2 st a in B2 & p in a & a c= A

      proof

        let A be Subset of T2;

        assume A is open;

        then

         A21: [:( [#] T1), A:] is open by BORSUK_1: 6;

        set p1 = the Point of T1;

        

         A22: p1 in ( [#] t1);

        let p2 be Point of T2;

        assume p2 in A;

        then

         A23: [p1, p2] in [:( [#] T1), A:] by A22, ZFMISC_1: 87;

        then

        reconsider p = [p1, p2] as Point of T12;

        consider a12 be Subset of T12 such that

         A24: a12 in B12 and

         A25: p in a12 and

         A26: a12 c= [:( [#] T1), A:] by A21, A23, YELLOW_9: 31;

        p1 in ( [#] t1) & p2 in ( [#] t2);

        then

         A27: (PR2 . (p1,p2)) = p2 by FUNCT_3:def 5;

        a12 is open by A3, A24;

        then

        reconsider a = F2(a12) as open Subset of T2 by BORSUK_1: 18;

        take a;

        ( dom PR2) = [:( [#] T1), ( [#] T2):] by FUNCT_3:def 5

        .= ( [#] T12) by BORSUK_1:def 2;

        hence a in B2 & p2 in a by A19, A24, A25, A27, FUNCT_1:def 6;

        let y be object;

        assume y in a;

        then

        consider x be object such that

         A28: x in ( dom PR2) and

         A29: x in a12 & y = (PR2 . x) by FUNCT_1:def 6;

        consider x1,x2 be object such that

         A30: x1 in ( [#] T1) & x2 in ( [#] T2) and

         A31: x = [x1, x2] by A28, ZFMISC_1:def 2;

        (PR2 . (x1,x2)) = x2 by A30, FUNCT_3:def 5;

        hence thesis by A26, A29, A31, ZFMISC_1: 87;

      end;

      B2 c= the topology of T2

      proof

        let x be object;

        assume x in B2;

        then

        consider w be Subset of T12 such that

         A32: x = F2(w) and

         A33: PP[w] by A19;

        w is open by A3, A33;

        then F2(w) is open by BORSUK_1: 18;

        hence thesis by A32;

      end;

      then

      reconsider B2 as Basis of T2 by A20, YELLOW_9: 32;

      

       A34: ( card { F2(w) where w be Subset of T12 : PP[w] }) c= ( card B12) from BORSUK_2:sch 1;

      ( weight T2) c= ( card B2) by WAYBEL23: 73;

      hence thesis by A1, A19, A34;

    end;

    registration

      let T1,T2 be second-countable TopSpace;

      cluster [:T1, T2:] -> second-countable;

      coherence

      proof

        ( weight T1) c= omega & ( weight T2) c= omega by WAYBEL23:def 6;

        then

         A1: (( weight T1) *` ( weight T2)) c= omega by CARD_2: 90, CARD_4: 6;

        ( weight [:T1, T2:]) c= (( weight T1) *` ( weight T2)) by Th5;

        then ( weight [:T1, T2:]) c= omega by A1;

        hence thesis by WAYBEL23:def 6;

      end;

    end

    theorem :: METRIZTS:7

    

     Th7: ( card (F | A)) c= ( card F)

    proof

      set FA = (F | A);

      per cases ;

        suppose FA is empty;

        hence thesis;

      end;

        suppose

         A1: FA is non empty;

        deffunc F( set) = ($1 /\ A);

        

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

        

         A3: for x be set st x in F holds F(x) in FA

        proof

          let x be set;

          

           A4: F(x) c= A by XBOOLE_1: 17;

          assume x in F;

          hence thesis by A2, A4, TOPS_2:def 3;

        end;

        consider g be Function of F, FA such that

         A5: for x be set st x in F holds (g . x) = F(x) from FUNCT_2:sch 11( A3);

        

         A6: ( dom g) = F by A1, FUNCT_2:def 1;

        FA c= ( rng g)

        proof

          let x be object;

          assume x in FA;

          then

          consider B such that

           A7: B in F and

           A8: F(B) = x by TOPS_2:def 3;

          x = (g . B) by A5, A7, A8;

          hence thesis by A6, A7, FUNCT_1:def 3;

        end;

        hence thesis by A6, CARD_1: 12;

      end;

    end;

    theorem :: METRIZTS:8

    

     Th8: for Bas be Basis of T holds (Bas | A) is Basis of (T | A)

    proof

      let Bas be Basis of T;

      set BasA = (Bas | A);

      set TA = (T | A);

      

       A1: for U be Subset of TA st U is open holds for p be Point of TA st p in U holds ex a be Subset of TA st a in BasA & p in a & a c= U

      proof

        let U be Subset of TA;

        assume U is open;

        then

        consider W be Subset of T such that

         A2: W is open and

         A3: U = (W /\ the carrier of TA) by TSP_1:def 1;

        let p be Point of TA such that

         A4: p in U;

        p in W by A3, A4, XBOOLE_0:def 4;

        then

        consider Wb be Subset of T such that

         A5: Wb in Bas and

         A6: p in Wb and

         A7: Wb c= W by A2, YELLOW_9: 31;

        

         A8: (Wb /\ A) in BasA by A5, TOPS_2: 31;

        then

        reconsider WbA = (Wb /\ A) as Subset of TA;

        

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

        then p in WbA by A4, A6, XBOOLE_0:def 4;

        hence thesis by A3, A7, A8, A9, XBOOLE_1: 26;

      end;

      BasA c= the topology of TA

      proof

        let x be object such that

         A10: x in BasA;

        reconsider U = x as Subset of TA by A10;

        BasA is open by TOPS_2: 37;

        then U is open by A10;

        hence thesis;

      end;

      hence thesis by A1, YELLOW_9: 32;

    end;

    registration

      let T be second-countable TopSpace;

      let A be Subset of T;

      cluster (T | A) -> second-countable;

      coherence

      proof

        consider B be Basis of T such that

         A1: ( card B) = ( weight T) by WAYBEL23: 74;

        (B | A) is Basis of (T | A) by Th8;

        then

         A2: ( weight (T | A)) c= ( card (B | A)) by WAYBEL23: 73;

        ( card (B | A)) c= ( card B) by Th7;

        then ( weight T) c= omega & ( weight (T | A)) c= ( weight T) by A1, A2, WAYBEL23:def 6;

        then ( weight (T | A)) c= omega ;

        hence thesis by WAYBEL23:def 6;

      end;

    end

    registration

      let M be non empty MetrSpace;

      let A be non empty Subset of ( TopSpaceMetr M);

      cluster ( dist_min A) -> continuous;

      coherence

      proof

        set d = ( dist_min A);

        set TM = ( TopSpaceMetr M);

        

         A1: for P be Subset of R^1 st P is open holds (d " P) is open

        proof

          let P be Subset of R^1 ;

          assume

           A2: P is open;

          for p be Point of M st p in (d " P) holds ex r be Real st r > 0 & ( Ball (p,r)) c= (d " P)

          proof

            reconsider P9 = P as open Subset of ( TopSpaceMetr RealSpace ) by A2, TOPMETR:def 6;

            let p be Point of M;

            assume p in (d " P);

            then

             A3: (d . p) in P by FUNCT_1:def 7;

            then

            reconsider dp = (d . p) as Point of RealSpace by TOPMETR:def 6;

            consider r be Real such that

             A4: r > 0 and

             A5: ( Ball (dp,r)) c= P9 by A3, TOPMETR: 15;

            take r;

            thus r > 0 by A4;

            thus ( Ball (p,r)) c= (d " P)

            proof

              let x be object;

              assume

               A6: x in ( Ball (p,r));

              then

              reconsider q = x as Point of M;

              

               A7: ( dist (p,q)) < r by A6, METRIC_1: 11;

              

               A8: ( dom d) = ( [#] M) by FUNCT_2:def 1;

              then (d . q) in ( rng d) by FUNCT_1:def 3;

              then

              reconsider dq = (d . q) as Point of RealSpace by TOPMETR:def 6;

              (d . q) <= (( dist (q,p)) + (d . p)) by HAUSDORF: 15;

              then ((d . q) - (d . p)) <= ( dist (p,q)) by XREAL_1: 20;

              then

               A9: ( - ( dist (p,q))) <= ( - ((d . q) - (d . p))) by XREAL_1: 24;

              (d . p) <= (( dist (p,q)) + (d . q)) by HAUSDORF: 15;

              then ((d . p) - (d . q)) <= ( dist (p,q)) by XREAL_1: 20;

              then |.((d . p) - (d . q)).| <= ( dist (p,q)) by A9, ABSVALUE: 5;

              then |.((d . p) - (d . q)).| < r by A7, XXREAL_0: 2;

              then ( dist (dp,dq)) < r by METRIC_1:def 12;

              then dq in ( Ball (dp,r)) by METRIC_1: 11;

              hence thesis by A5, A8, FUNCT_1:def 7;

            end;

          end;

          hence thesis by TOPMETR: 15;

        end;

        ( [#] R^1 ) = {} implies ( [#] TM) = {} ;

        hence thesis by A1, TOPS_2: 43;

      end;

    end

    theorem :: METRIZTS:9

    for B be Subset of T, F be Subset of (T | A) st F = B holds ((T | A) | F) = (T | B)

    proof

      let B be Subset of T, F be Subset of (T | A) such that

       A1: F = B;

      ((T | A) | F) is SubSpace of T & ( [#] ((T | A) | F)) = F by PRE_TOPC:def 5, TSEP_1: 7;

      hence thesis by A1, PRE_TOPC:def 5;

    end;

    

     Lm4: for M be non empty MetrSpace holds for A be non empty Subset of ( TopSpaceMetr M), r be Real holds { p where p be Point of ( TopSpaceMetr M) : (( dist_min A) . p) < r } is open Subset of ( TopSpaceMetr M)

    proof

      let M be non empty MetrSpace;

      set TM = ( TopSpaceMetr M);

      let A be non empty Subset of TM, r be Real;

      set d = ( dist_min A);

      reconsider A = ]. -infty , r.[ as Subset of R^1 by TOPMETR: 17;

      set dA = { p where p be Point of TM : (d . p) < r };

      

       A1: dA c= (d " A)

      proof

        let x be object;

        assume x in dA;

        then

        consider p be Point of TM such that

         A2: p = x and

         A3: (d . p) < r;

        ( dom d) = ( [#] TM) & (d . p) in A by A3, FUNCT_2:def 1, XXREAL_1: 233;

        hence thesis by A2, FUNCT_1:def 7;

      end;

      

       A4: (d " A) c= dA

      proof

        let x be object;

        assume

         A5: x in (d " A);

        then

        reconsider p = x as Point of TM;

        (d . p) in A by A5, FUNCT_1:def 7;

        then (d . p) < r by XXREAL_1: 233;

        hence thesis;

      end;

      

       A6: A is open by BORSUK_5: 40;

      ( [#] R^1 ) = {} implies ( [#] TM) = {} ;

      then (d " A) is open by A6, TOPS_2: 43;

      hence thesis by A1, A4, XBOOLE_0:def 10;

    end;

    registration

      let TM;

      cluster open -> F_sigma for Subset of TM;

      coherence

      proof

        set TOP = the topology of TM, cTM = the carrier of TM;

        let Am;

        assume

         A1: Am is open;

        per cases ;

          suppose

           A2: TM is empty;

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

          Am = ( union E) by A2, ZFMISC_1: 2;

          hence thesis by TOPGEN_4:def 6;

        end;

          suppose

           A3: TM is non empty;

          per cases ;

            suppose Am = ( [#] TM);

            hence thesis by A3;

          end;

            suppose

             A4: Am <> ( [#] TM);

            consider metr be Function of [:cTM, cTM:], REAL such that

             A5: metr is_metric_of cTM and

             A6: ( Family_open_set ( SpaceMetr (cTM,metr))) = TOP by PCOMPS_1:def 8;

            reconsider Tm = ( SpaceMetr (cTM,metr)) as non empty MetrSpace by A3, A5, PCOMPS_1: 36;

            set TTm = ( TopSpaceMetr Tm);

            Am in the topology of TTm by A1, A6;

            then

            reconsider a = Am as open Subset of TTm by PRE_TOPC:def 2;

            (( {} TTm) ` ) = ( [#] TTm);

            then

            reconsider A9 = (a ` ) as closed non empty Subset of TTm by A3, A4, A5, PCOMPS_2: 4;

            defpred P[ object, object] means for n be Nat st n = $1 holds $2 = { p where p be Point of TTm : (( dist_min A9) . p) < (1 / (2 |^ n)) };

            

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

            proof

              let x be object;

              assume x in NAT ;

              then

              reconsider n = x as Element of NAT ;

              reconsider BallA = { p where p be Point of TTm : (( dist_min A9) . p) < (1 / (2 |^ n)) } as open Subset of TTm by Lm4;

              take BallA;

              thus thesis by A6, PRE_TOPC:def 2;

            end;

            consider p be sequence of TOP such that

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

            reconsider RNG = ( rng p) as open Subset-Family of TM by TOPS_2: 11, XBOOLE_1: 1;

            set Crng = ( COMPLEMENT RNG);

            

             A9: ( dom p) = NAT by FUNCT_2:def 1;

            

             A10: ( [#] TM) = ( [#] TTm) by A3, A5, PCOMPS_2: 4;

            

             A11: ( union Crng) = Am

            proof

              hereby

                let x be object;

                assume

                 A12: x in ( union Crng);

                then

                consider y be set such that

                 A13: x in y and

                 A14: y in ( COMPLEMENT RNG) by TARSKI:def 4;

                reconsider Y = y as Subset of TM by A14;

                (Y ` ) in RNG by A14, SETFAM_1:def 7;

                then

                consider n be object such that

                 A15: n in ( dom p) and

                 A16: (p . n) = (Y ` ) by FUNCT_1:def 3;

                reconsider n as Element of NAT by A15;

                assume not x in Am;

                then x in A9 by A10, A12, XBOOLE_0:def 5;

                then

                 A17: (2 |^ n) > 0 & (( dist_min A9) . x) = 0 by HAUSDORF: 5, PREPOWER: 6;

                (Y ` ) = { q where q be Point of TTm : (( dist_min A9) . q) < (1 / (2 |^ n)) } by A8, A16;

                then x in (Y ` ) by A10, A12, A17;

                hence contradiction by A13, XBOOLE_0:def 5;

              end;

              let x be object;

              assume

               A18: x in Am;

              then

              reconsider q = x as Point of TTm by A3, A5, PCOMPS_2: 4;

              ( Cl A9) = A9 & not q in A9 by A18, PRE_TOPC: 22, XBOOLE_0:def 5;

              then

               A19: (( dist_min A9) . q) <> 0 by HAUSDORF: 8;

              (( dist_min A9) . q) >= 0 by JORDAN1K: 9;

              then

              consider n be Nat such that

               A20: (1 / (2 |^ n)) <= (( dist_min A9) . q) by A19, PREPOWER: 92;

              

               A21: n in NAT by ORDINAL1:def 12;

              (p . n) in RNG by A9, FUNCT_1:def 3, A21;

              then

              reconsider pn = (p . n) as Subset of TM;

              

               A22: pn = { s where s be Point of TTm : (( dist_min A9) . s) < (1 / (2 |^ n)) } by A8, A21;

              for s be Point of TTm st s = q holds not (1 / (2 |^ n)) > (( dist_min A9) . s) by A20;

              then not q in pn by A22;

              then

               A23: q in (pn ` ) by A18, XBOOLE_0:def 5;

              ((pn ` ) ` ) in RNG by A9, FUNCT_1:def 3, A21;

              then (pn ` ) in Crng by SETFAM_1:def 7;

              hence thesis by A23, TARSKI:def 4;

            end;

            Crng is closed & RNG is countable by A9, CARD_3: 93, TOPS_2: 10;

            hence thesis by A11, TOPGEN_4:def 6;

          end;

        end;

      end;

      cluster closed -> G_delta for Subset of TM;

      coherence

      proof

        let Am;

        assume

         A24: Am is closed;

        per cases ;

          suppose

           A25: TM is empty;

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

          Am = ( meet E) by A25, SETFAM_1: 1;

          hence thesis by TOPGEN_4:def 7;

        end;

          suppose TM is non empty;

          then ((Am ` ) ` ) is G_delta by A24, TOPGEN_4: 37;

          hence thesis;

        end;

      end;

    end

    theorem :: METRIZTS:10

    for F be Subset of (T | B) st A is F_sigma & F = (A /\ B) holds F is F_sigma

    proof

      let F be Subset of (T | B);

      assume that

       A1: A is F_sigma and

       A2: F = (A /\ B);

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

       A3: A = ( union G) by A1, TOPGEN_4:def 6;

      

       A4: ( union (G | B)) c= F

      proof

        let x be object;

        assume x in ( union (G | B));

        then

        consider g be set such that

         A5: x in g and

         A6: g in (G | B) by TARSKI:def 4;

        consider h be Subset of T such that

         A7: h in G and

         A8: (h /\ B) = g by A6, TOPS_2:def 3;

        x in h by A5, A8, XBOOLE_0:def 4;

        then

         A9: x in A by A3, A7, TARSKI:def 4;

        x in B by A5, A8, XBOOLE_0:def 4;

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

      end;

      ( card (G | B)) c= ( card G) & ( card G) c= omega by Th7, CARD_3:def 14;

      then ( card (G | B)) c= omega ;

      then

       A10: (G | B) is closed & (G | B) is countable by TOPS_2: 38;

      ((A /\ B) /\ B) = (A /\ (B /\ B)) by XBOOLE_1: 16

      .= F by A2;

      then F c= ( union (G | B)) by A3, TOPS_2: 32, XBOOLE_1: 17;

      then F = ( union (G | B)) by A4;

      hence thesis by A10, TOPGEN_4:def 6;

    end;

    theorem :: METRIZTS:11

    for F be Subset of (T | B) st A is G_delta & F = (A /\ B) holds F is G_delta

    proof

      let F be Subset of (T | B);

      assume that

       A1: A is G_delta and

       A2: F = (A /\ B);

      consider G be open countable Subset-Family of T such that

       A3: A = ( meet G) by A1, TOPGEN_4:def 7;

      

       A4: ( meet (G | B)) c= F

      proof

        let x be object;

        assume

         A5: x in ( meet (G | B));

        then

        consider g be object such that

         A6: g in (G | B) by SETFAM_1: 1, XBOOLE_0:def 1;

        reconsider g as Subset of (T | B) by A6;

        

         A7: ex h be Subset of T st h in G & (h /\ B) = g by A6, TOPS_2:def 3;

        x in g by A5, A6, SETFAM_1:def 1;

        then

         A8: x in B by A7, XBOOLE_0:def 4;

        now

          let Y be set;

          assume Y in G;

          then (Y /\ B) in (G | B) by TOPS_2: 31;

          then x in (Y /\ B) by A5, SETFAM_1:def 1;

          hence x in Y by XBOOLE_0:def 4;

        end;

        then x in A by A3, A7, SETFAM_1:def 1;

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

      end;

      ( card (G | B)) c= ( card G) & ( card G) c= omega by Th7, CARD_3:def 14;

      then ( card (G | B)) c= omega ;

      then

       A9: (G | B) is open & (G | B) is countable by TOPS_2: 37;

      F c= ( meet (G | B))

      proof

        let x be object;

        assume

         A10: x in F;

        then

         A11: x in A by A2, XBOOLE_0:def 4;

        

         A12: x in B by A2, A10, XBOOLE_0:def 4;

         A13:

        now

          let f be set;

          assume f in (G | B);

          then

          consider h be Subset of T such that

           A14: h in G and

           A15: (h /\ B) = f by TOPS_2:def 3;

          x in h by A3, A11, A14, SETFAM_1:def 1;

          hence x in f by A12, A15, XBOOLE_0:def 4;

        end;

        ex y be object st y in G by A3, A11, SETFAM_1: 1, XBOOLE_0:def 1;

        then (G | B) is non empty by TOPS_2: 31;

        hence thesis by A13, SETFAM_1:def 1;

      end;

      then F = ( meet (G | B)) by A4;

      hence thesis by A9, TOPGEN_4:def 7;

    end;

    theorem :: METRIZTS:12

    

     Th12: T is T_1 & A is discrete implies A is open Subset of (T | ( Cl A))

    proof

      assume that

       A1: T is T_1 and

       A2: A is discrete;

      set TA = (T | ( Cl A));

      

       A3: ( [#] TA) = ( Cl A) by PRE_TOPC:def 5;

      

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

      per cases ;

        suppose TA is empty;

        hence thesis by A3, PRE_TOPC: 18;

      end;

        suppose TA is non empty;

        then

        reconsider TA as non empty TopSpace;

        deffunc F( Element of TA) = {$1};

        defpred P[ set] means $1 in A;

        consider S be Subset-Family of TA such that

         A5: S = { F(x) where x be Element of TA : P[x] } from LMOD_7:sch 5;

        

         A6: S is open

        proof

          let B be Subset of TA;

          assume B in S;

          then

          consider y be Element of TA such that

           A7: B = F(y) and

           A8: P[y] by A5;

          reconsider x = y as Point of T by A8;

          consider G be Subset of T such that

           A9: G is open and

           A10: (A /\ G) = {x} by A2, A8, TEX_2: 26;

          reconsider X = {x} as Subset of T by A10;

          T is non empty by A7;

          then

           A11: ( Cl X) = X by A1, PRE_TOPC: 22;

          x in {x} by TARSKI:def 1;

          then x in A & x in G by A10, XBOOLE_0:def 4;

          then

           A12: (G /\ ( Cl A)) <> {} by A4, XBOOLE_0:def 4;

          (G /\ ( Cl A)) c= ( Cl X) by A9, A10, TOPS_1: 13;

          then (G /\ ( Cl A)) = X by A11, A12, ZFMISC_1: 33;

          hence thesis by A3, A7, A9, TSP_1:def 1;

        end;

        ( union S) = A

        proof

          hereby

            let x be object;

            assume x in ( union S);

            then

            consider y be set such that

             A13: x in y and

             A14: y in S by TARSKI:def 4;

            ex z be Element of TA st F(z) = y & P[z] by A5, A14;

            hence x in A by A13, TARSKI:def 1;

          end;

          let x be object;

          assume x in A;

          then

           A15: {x} in S by A3, A4, A5;

          x in {x} by TARSKI:def 1;

          hence thesis by A15, TARSKI:def 4;

        end;

        hence thesis by A6, TOPS_2: 19;

      end;

    end;

    

     Lm5: ( omega *` iC) = iC

    proof

       omega c= iC by CARD_3: 85;

      then

       A1: ( omega *` iC) c= (iC *` iC) by CARD_2: 90;

      (iC *` iC) = iC & iC c= ( omega *` iC) by CARD_2: 95, CARD_4: 15;

      hence thesis by A1;

    end;

    theorem :: METRIZTS:13

    

     Th13: for T st for F st F is open & F is Cover of T holds ex G st G c= F & G is Cover of T & ( card G) c= C holds for A st A is closed & A is discrete holds ( card A) c= C

    proof

      let T;

      assume

       A1: for F st F is open & F is Cover of T holds ex G st G c= F & G is Cover of T & ( card G) c= C;

      set TOP = the topology of T;

      let A such that

       A2: A is closed and

       A3: A is discrete;

      (A ` ) in TOP by A2, PRE_TOPC:def 2;

      then

       A4: {(A ` )} c= TOP by ZFMISC_1: 31;

      defpred Q[ object, object] means ex D1 be set st D1 = $1 & {$2} = (D1 /\ A);

      defpred P[ object, object] means ex D2 be set st D2 = $2 & (A /\ D2) = {$1};

      

       A5: for x be object st x in A holds ex y be object st y in TOP & P[x, y]

      proof

        let x be object;

        assume x in A;

        then

        consider G be Subset of T such that

         A6: G is open & (A /\ G) = {x} by A3, TEX_2: 26;

        take G;

        thus thesis by A6;

      end;

      consider p be Function of A, TOP such that

       A7: for x be object st x in A holds P[x, (p . x)] from FUNCT_2:sch 1( A5);

      reconsider RNG = ( rng p), AA = {(A ` )} as open Subset-Family of T by A4, TOPS_2: 11, XBOOLE_1: 1;

      reconsider RngA = (RNG \/ AA) as open Subset-Family of T by TOPS_2: 13;

      ( [#] T) c= ( union RngA)

      proof

        let x be object;

        assume

         A8: x in ( [#] T);

        per cases ;

          suppose

           A9: x in A;

          ( dom p) = A by FUNCT_2:def 1;

          then (p . x) in ( rng p) by A9, FUNCT_1:def 3;

          then

           A10: (p . x) in RngA by XBOOLE_0:def 3;

           P[x, (p . x)] by A7, A9;

          then x in {x} & (A /\ (p . x)) = {x} by TARSKI:def 1;

          then x in (p . x) by XBOOLE_0:def 4;

          hence thesis by A10, TARSKI:def 4;

        end;

          suppose

           A11: not x in A;

          (A ` ) in AA by TARSKI:def 1;

          then

           A12: (A ` ) in RngA by XBOOLE_0:def 3;

          x in (A ` ) by A8, A11, XBOOLE_0:def 5;

          hence thesis by A12, TARSKI:def 4;

        end;

      end;

      then RngA is Cover of T by SETFAM_1:def 11;

      then

      consider G be Subset-Family of T such that

       A13: G c= RngA and

       A14: G is Cover of T and

       A15: ( card G) c= C by A1;

      

       A16: for x be object st x in (G \ AA) holds ex y be object st y in A & Q[x, y]

      proof

        let x be object;

        assume x in (G \ AA);

        then x in G & not x in AA by XBOOLE_0:def 5;

        then x in RNG by A13, XBOOLE_0:def 3;

        then

        consider y be object such that

         A17: y in ( dom p) & (p . y) = x by FUNCT_1:def 3;

        take y;

         P[y, (p . y)] by A7, A17;

        hence thesis by A17;

      end;

      consider q be Function of (G \ AA), A such that

       A18: for x be object st x in (G \ AA) holds Q[x, (q . x)] from FUNCT_2:sch 1( A16);

      per cases ;

        suppose A is empty;

        hence thesis;

      end;

        suppose A is non empty;

        then

         A19: ( dom q) = (G \ AA) by FUNCT_2:def 1;

        A c= ( rng q)

        proof

          let x be object such that

           A20: x in A;

          T is non empty by A20;

          then

          consider U be Subset of T such that

           A21: x in U and

           A22: U in G by A14, A20, PCOMPS_1: 3;

           not x in (A ` ) by A20, XBOOLE_0:def 5;

          then not U in AA by A21, TARSKI:def 1;

          then

           A23: U in (G \ AA) by A22, XBOOLE_0:def 5;

          then Q[U, (q . U)] by A18;

          then

           A24: (q . U) in ( rng q) & {(q . U)} = (U /\ A) by A19, FUNCT_1:def 3, A23;

          x in (A /\ U) by A20, A21, XBOOLE_0:def 4;

          hence thesis by A24, TARSKI:def 1;

        end;

        then

         A25: ( card A) c= ( card (G \ AA)) by A19, CARD_1: 12;

        ( card (G \ AA)) c= ( card G) by CARD_1: 11, XBOOLE_1: 36;

        then ( card A) c= ( card G) by A25;

        hence ( card A) c= C by A15;

      end;

    end;

    theorem :: METRIZTS:14

    

     Th14: for TM st for Am st Am is closed & Am is discrete holds ( card Am) c= iC holds for Am st Am is discrete holds ( card Am) c= iC

    proof

      let TM;

      assume

       A1: for Am st Am is closed & Am is discrete holds ( card Am) c= iC;

      let Am such that

       A2: Am is discrete;

      per cases ;

        suppose Am is empty;

        hence thesis;

      end;

        suppose

         A3: Am is non empty;

        then

        reconsider Tm = TM as metrizable non empty TopSpace;

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

        then

        reconsider ClA = ( Cl Am) as non empty closed Subset of Tm by A3;

        set TA = (Tm | ClA);

        reconsider A9 = Am as open Subset of TA by A2, Th12;

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

         A4: A9 = ( union F) by TOPGEN_4:def 6;

        consider f be sequence of F such that

         A5: ( rng f) = F by A3, A4, CARD_3: 96, ZFMISC_1: 2;

        

         A6: for x be object st x in ( dom f) holds ( card (f . x)) c= iC

        proof

          let x be object;

          assume x in ( dom f);

          then

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

          then

          reconsider fx = (f . x) as Subset of TA by A5;

          

           A8: (f . x) c= Am by A4, A7, ZFMISC_1: 74;

          then

          reconsider Fx = (f . x) as Subset of TM by XBOOLE_1: 1;

          ( [#] TA) = ClA & fx is closed by A7, PRE_TOPC:def 5, TOPS_2:def 2;

          then Fx is closed by TSEP_1: 8;

          hence thesis by A1, A2, A8, TEX_2: 22;

        end;

        ( card ( dom f)) = omega by A3, A4, CARD_1: 47, FUNCT_2:def 1, ZFMISC_1: 2;

        then ( card ( Union f)) c= ( omega *` iC) by A6, CARD_2: 86;

        hence thesis by A4, A5, Lm5;

      end;

    end;

    theorem :: METRIZTS:15

    

     Th15: for T st for A st A is discrete holds ( card A) c= C holds for F st F is open & not {} in F & for A, B st A in F & B in F & A <> B holds A misses B holds ( card F) c= C

    proof

      let T;

      assume

       A1: for A st A is discrete holds ( card A) c= C;

      let F such that

       A2: F is open and

       A3: not {} in F and

       A4: for A, B st A in F & B in F & A <> B holds A misses B;

      per cases ;

        suppose F is empty;

        hence thesis;

      end;

        suppose

         A5: F is non empty;

        deffunc P( set) = the Element of $1;

        

         A6: for x be set st x in F holds P(x) in ( [#] T)

        proof

          let x be set;

          assume

           A7: x in F;

          then x <> {} by A3;

          then P(x) in x;

          hence thesis by A7;

        end;

        consider p be Function of F, ( [#] T) such that

         A8: for x be set st x in F holds (p . x) = P(x) from FUNCT_2:sch 11( A6);

        reconsider RNG = ( rng p) as Subset of T;

        ex xx be object st xx in F by A5;

        then

         A9: T is non empty by A3;

        then

         A10: ( dom p) = F by FUNCT_2:def 1;

        for x be Point of T st x in RNG holds ex G be Subset of T st G is open & (RNG /\ G) = {x}

        proof

          let x be Point of T;

          assume

           A11: x in RNG;

          then

          consider G be object such that

           A12: G in F and

           A13: (p . G) = x by A10, FUNCT_1:def 3;

          reconsider G as Subset of T by A12;

          

           A14: (RNG /\ G) c= {x}

          proof

            let y be object;

            assume

             A15: y in (RNG /\ G);

            then

             A16: y in G by XBOOLE_0:def 4;

            y in RNG by A15, XBOOLE_0:def 4;

            then

            consider z be object such that

             A17: z in F and

             A18: (p . z) = y by A10, FUNCT_1:def 3;

            reconsider z as set by TARSKI: 1;

            y = P(z) by A8, A17, A18;

            then z meets G by A3, A16, A17, XBOOLE_0: 3;

            then x = y by A4, A12, A13, A17, A18;

            hence thesis by TARSKI:def 1;

          end;

          take G;

          thus G is open by A2, A12;

          x = P(G) by A8, A12, A13;

          then x in (RNG /\ G) by A3, A11, A12, XBOOLE_0:def 4;

          hence thesis by A14, ZFMISC_1: 33;

        end;

        then

         A19: ( card RNG) c= C by A1, A9, TEX_2: 31;

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

        proof

          let x1,x2 be object such that

           A20: x1 in ( dom p) and

           A21: x2 in ( dom p) and

           A22: (p . x1) = (p . x2);

          reconsider x1, x2 as set by TARSKI: 1;

          

           A23: (p . x2) = P(x2) & x2 <> {} by A3, A8, A21;

          (p . x1) = P(x1) & x1 <> {} by A3, A8, A20;

          then x1 meets x2 by A22, A23, XBOOLE_0: 3;

          hence thesis by A4, A10, A20, A21;

        end;

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

        then ( card F) c= ( card RNG) by A10, CARD_1: 10;

        hence thesis by A19;

      end;

    end;

    theorem :: METRIZTS:16

    

     Th16: for F st F is Cover of T holds ex G st G c= F & G is Cover of T & ( card G) c= ( card ( [#] T))

    proof

      let F such that

       A1: F is Cover of T;

      per cases ;

        suppose

         A2: F is empty;

        take F;

        thus thesis by A1, A2;

      end;

        suppose

         A3: F is non empty;

        defpred P[ object, object] means ex D2 be set st D2 = $2 & $1 in D2;

        

         A4: for x be object st x in ( [#] T) holds ex y be object st y in F & P[x, y]

        proof

          let x be object;

          assume x in ( [#] T);

          then x in ( union F) by A1, SETFAM_1: 45;

          then ex y be set st x in y & y in F by TARSKI:def 4;

          hence thesis;

        end;

        consider g be Function of ( [#] T), F such that

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

        reconsider R = ( rng g) as Subset-Family of T by XBOOLE_1: 1;

        take R;

        

         A6: ( dom g) = ( [#] T) by A3, FUNCT_2:def 1;

        ( [#] T) c= ( union R)

        proof

          let x be object;

          assume

           A7: x in ( [#] T);

          then P[x, (g . x)] by A5;

          then x in (g . x) & (g . x) in R by A6, FUNCT_1:def 3, A7;

          hence thesis by TARSKI:def 4;

        end;

        hence thesis by A6, CARD_1: 12, SETFAM_1:def 11;

      end;

    end;

    

     Lm6: (for Fm st Fm is open & not {} in Fm & for Am, Bm st Am in Fm & Bm in Fm & Am <> Bm holds Am misses Bm holds ( card Fm) c= iC) implies ( density TM) c= iC

    proof

      assume

       A1: for Fm st Fm is open & not {} in Fm & for Am, Bm st Am in Fm & Bm in Fm & Am <> Bm holds Am misses Bm holds ( card Fm) c= iC;

      per cases ;

        suppose

         A2: TM is empty;

        ex D be Subset of TM st D is dense & ( density TM) = ( card D) by TOPGEN_1:def 12;

        hence thesis by A2;

      end;

        suppose

         A3: TM is non empty;

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

         A4: metr is_metric_of the carrier of TM and

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

        reconsider M = ( SpaceMetr (the carrier of TM,metr)) as non empty MetrSpace by A3, A4, PCOMPS_1: 36;

        defpred P[ object, object] means for n be Nat st $1 = n holds ex G be Subset of TM st G = $2 & ( card G) c= iC & for p be Element of M holds ex q be Element of M st q in G & ( dist (p,q)) < (1 / (2 |^ n));

        

         A6: the carrier of TM = the carrier of M by A3, A4, PCOMPS_2: 4;

        

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

        proof

          let x be object;

          assume x in NAT ;

          then

          reconsider n = x as Element of NAT ;

          reconsider r = (1 / (2 |^ n)) as Real;

          

           A8: (2 |^ n) > 0 by PREPOWER: 6;

          then

          consider A be Subset of M such that

           A9: for p,q be Point of M st p <> q & p in A & q in A holds ( dist (p,q)) >= r and

           A10: for p be Point of M holds ex q be Point of M st q in A & p in ( Ball (q,r)) by COMPL_SP: 30;

          set BALL = { ( Ball (p,(r / 2))) where p be Element of M : p in A };

          

           A11: BALL c= the topology of TM

          proof

            let x be object;

            assume x in BALL;

            then ex p be Point of M st x = ( Ball (p,(r / 2))) & p in A;

            hence thesis by A5, PCOMPS_1: 29;

          end;

          reconsider BALL as open Subset-Family of TM by A11, TOPS_2: 11, XBOOLE_1: 1;

          defpred Q[ object, object] means for p be Point of M st ( Ball (p,(r / 2))) = $1 & p in A holds p = $2;

          

           A12: for x be object st x in BALL holds ex y be object st y in A & Q[x, y]

          proof

            let x be object;

            assume x in BALL;

            then

            consider p be Point of M such that

             A13: x = ( Ball (p,(r / 2))) and

             A14: p in A;

            

             A15: (r / 2) < r by A8, XREAL_1: 216;

            take p;

            thus p in A by A14;

            let q be Point of M such that

             A16: ( Ball (q,(r / 2))) = x and

             A17: q in A;

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

            then p in ( Ball (p,(r / 2))) by A8, METRIC_1: 11;

            then ( dist (q,p)) < (r / 2) by A13, A16, METRIC_1: 11;

            then ( dist (q,p)) < r by A15, XXREAL_0: 2;

            hence thesis by A9, A14, A17;

          end;

          consider f be Function of BALL, A such that

           A18: for x be object st x in BALL holds Q[x, (f . x)] from FUNCT_2:sch 1( A12);

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

          ex q be Point of M st q in A & the Point of M in ( Ball (q,r)) by A10;

          then

           A19: ( dom f) = BALL by FUNCT_2:def 1;

          then

           A20: ( card RNG) c= ( card BALL) by CARD_1: 12;

          

           A21: for A9,B9 be Subset of TM st A9 in BALL & B9 in BALL & A9 <> B9 holds A9 misses B9

          proof

            let A9,B9 be Subset of TM such that

             A22: A9 in BALL and

             A23: B9 in BALL and

             A24: A9 <> B9;

            consider b be Element of M such that

             A25: ( Ball (b,(r / 2))) = B9 and

             A26: b in A by A23;

            consider a be Element of M such that

             A27: ( Ball (a,(r / 2))) = A9 and

             A28: a in A by A22;

            assume A9 meets B9;

            then

            consider x be object such that

             A29: x in A9 and

             A30: x in B9 by XBOOLE_0: 3;

            reconsider x as Element of M by A27, A29;

            

             A31: ( dist (a,x)) < (r / 2) by A27, A29, METRIC_1: 11;

            ( dist (b,x)) < (r / 2) by A25, A30, METRIC_1: 11;

            then

             A32: ( dist (a,b)) <= (( dist (a,x)) + ( dist (x,b))) & (( dist (a,x)) + ( dist (x,b))) < ((r / 2) + (r / 2)) by A31, METRIC_1: 4, XREAL_1: 8;

            ( dist (a,b)) >= r by A9, A24, A25, A26, A27, A28;

            hence thesis by A32, XXREAL_0: 2;

          end;

          take RNG;

          thus RNG in ( bool the carrier of TM);

          let m be Nat such that

           A33: x = m;

           A34:

          now

            let p be Element of M;

            consider q be Point of M such that

             A35: q in A and

             A36: p in ( Ball (q,r)) by A10;

            take q;

            

             A37: ( Ball (q,(r / 2))) in BALL by A35;

            then (f . ( Ball (q,(r / 2)))) = q by A18, A35;

            hence q in RNG & ( dist (p,q)) < (1 / (2 |^ m)) by A19, A33, A36, A37, FUNCT_1:def 3, METRIC_1: 11;

          end;

           not {} in BALL

          proof

            assume {} in BALL;

            then

            consider p be Element of M such that

             A38: ( Ball (p,(r / 2))) = {} and p in A;

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

            hence thesis by A8, A38, METRIC_1: 11;

          end;

          then ( card BALL) c= iC by A1, A21;

          hence thesis by A20, A34, XBOOLE_1: 1;

        end;

        consider p be sequence of ( bool the carrier of TM) such that

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

        reconsider Up = ( Union p) as Subset of TM;

        for U be Subset of TM st U <> {} & U is open holds Up meets U

        proof

          let U be Subset of TM;

          reconsider U9 = U as Subset of M by A3, A4, PCOMPS_2: 4;

          assume that

           A40: U <> {} and

           A41: U is open;

          consider q be object such that

           A42: q in U by A40, XBOOLE_0:def 1;

          reconsider q as Element of M by A3, A4, A42, PCOMPS_2: 4;

          U9 in ( Family_open_set M) by A5, A41;

          then

          consider r be Real such that

           A43: r > 0 and

           A44: ( Ball (q,r)) c= U9 by A42, PCOMPS_1:def 4;

          consider n be Nat such that

           A45: (1 / (2 |^ n)) <= r by A43, PREPOWER: 92;

          

           A46: n in NAT by ORDINAL1:def 12;

          consider G be Subset of TM such that

           A47: G = (p . n) and ( card G) c= iC and

           A48: for p be Element of M holds ex q be Element of M st q in G & ( dist (p,q)) < (1 / (2 |^ n)) by A39, A46;

          consider qq be Element of M such that

           A49: qq in G and

           A50: ( dist (q,qq)) < (1 / (2 |^ n)) by A48;

          ( dist (q,qq)) < r by A45, A50, XXREAL_0: 2;

          then

           A51: qq in ( Ball (q,r)) by METRIC_1: 11;

          qq in Up by A47, A49, PROB_1: 12;

          hence thesis by A44, A51, XBOOLE_0: 3;

        end;

        then Up is dense by TOPS_1: 45;

        then

         A52: ( density TM) c= ( card Up) by TOPGEN_1:def 12;

        

         A53: for x be object st x in ( dom p) holds ( card (p . x)) c= iC

        proof

          let x be object;

          assume x in ( dom p);

          then

          reconsider n = x as Element of NAT ;

          ex G be Subset of TM st G = (p . n) & ( card G) c= iC & for p be Element of M holds ex q be Element of M st q in G & ( dist (p,q)) < (1 / (2 |^ n)) by A39;

          hence thesis;

        end;

        ( card ( dom p)) = omega by CARD_1: 47, FUNCT_2:def 1;

        then

         A54: ( card Up) c= ( omega *` iC) by A53, CARD_2: 86;

        ( omega *` iC) = iC by Lm5;

        hence thesis by A52, A54;

      end;

    end;

    theorem :: METRIZTS:17

    

     Th17: Am is dense implies ( weight TM) c= ( omega *` ( card Am))

    proof

      assume

       A1: Am is dense;

      per cases ;

        suppose TM is empty;

        hence thesis;

      end;

        suppose

         A2: TM is non empty;

        set TOP = the topology of TM, cTM = the carrier of TM;

        consider metr be Function of [:cTM, cTM:], REAL such that

         A3: metr is_metric_of cTM and

         A4: ( Family_open_set ( SpaceMetr (cTM,metr))) = TOP by PCOMPS_1:def 8;

        reconsider Tm = ( SpaceMetr (cTM,metr)) as non empty MetrSpace by A2, A3, PCOMPS_1: 36;

        defpred P[ object, object] means ex D2 be set st D2 = $2 & for n be Nat st n = $1 holds $2 = { ( Ball (p,(1 / (2 |^ n)))) where p be Point of Tm : p in Am } & ( card D2) c= ( card Am);

        

         A5: for x be object st x in NAT holds ex y be object st y in ( bool TOP) & P[x, y]

        proof

          defpred P[ object] means not contradiction;

          let x be object;

          defpred P1[ object] means $1 in Am;

          defpred P2[ object] means $1 in Am & P[$1];

          assume x in NAT ;

          then

          reconsider n = x as Element of NAT ;

          deffunc F( Point of Tm) = ( Ball ($1,(1 / (2 |^ n))));

          set BALL1 = { F(p) where p be Point of Tm : P1[p] };

          set BALL2 = { F(p) where p be Point of Tm : P2[p] };

          take BALL1;

          

           A6: BALL1 c= TOP

          proof

            let y be object;

            assume y in BALL1;

            then ex p be Point of Tm st y = F(p) & P1[p];

            hence thesis by A4, PCOMPS_1: 29;

          end;

          

           A7: for p be Point of Tm holds P1[p] iff P2[p];

          

           A8: BALL1 = BALL2 from FRAENKEL:sch 3( A7);

          thus BALL1 in ( bool TOP) by A6;

          take BALL1;

          ( card BALL2) c= ( card Am) from BORSUK_2:sch 1;

          hence thesis by A8;

        end;

        consider P be sequence of ( bool TOP) such that

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

        reconsider Up = ( Union P) as Subset-Family of TM by XBOOLE_1: 1;

        

         A10: for B be Subset of TM st B is open holds for p be Point of TM st p in B holds ex a be Subset of TM st a in Up & p in a & a c= B

        proof

          let B be Subset of TM;

          assume B is open;

          then

           A11: B in TOP;

          let p be Point of TM such that

           A12: p in B;

          reconsider p9 = p as Point of Tm by A2, A3, PCOMPS_2: 4;

          consider r be Real such that

           A13: r > 0 and

           A14: ( Ball (p9,r)) c= B by A4, A11, A12, PCOMPS_1:def 4;

          consider n be Nat such that

           A15: (1 / (2 |^ n)) <= (r / 2) by A13, PREPOWER: 92;

          reconsider B2 = ( Ball (p9,(1 / (2 |^ n)))) as Subset of TM by A2, A3, PCOMPS_2: 4;

          (2 |^ n) > 0 & ( dist (p9,p9)) = 0 by METRIC_1: 1, PREPOWER: 6;

          then

           A16: p9 in B2 by METRIC_1: 11;

          B2 in TOP by A4, PCOMPS_1: 29;

          then B2 is open;

          then B2 meets Am by A1, A16, TOPS_1: 45;

          then

          consider q be object such that

           A17: q in B2 and

           A18: q in Am by XBOOLE_0: 3;

          

           A19: n in NAT by ORDINAL1:def 12;

          reconsider q as Point of Tm by A17;

          reconsider B3 = ( Ball (q,(1 / (2 |^ n)))) as Subset of TM by A2, A3, PCOMPS_2: 4;

          take B3;

           P[n, (P . n)] by A9, A19;

          then (P . n) = { ( Ball (t,(1 / (2 |^ n)))) where t be Point of Tm : t in Am };

          then B3 in (P . n) by A18;

          hence B3 in Up by PROB_1: 12;

          

           A20: ( dist (p9,q)) < (1 / (2 |^ n)) by A17, METRIC_1: 11;

          hence p in B3 by METRIC_1: 11;

          let y be object;

          assume

           A21: y in B3;

          then

          reconsider t = y as Point of Tm;

          ( dist (q,t)) < (1 / (2 |^ n)) by A21, METRIC_1: 11;

          then

           A22: ( dist (q,t)) < (r / 2) by A15, XXREAL_0: 2;

          ( dist (p9,q)) < (r / 2) by A15, A20, XXREAL_0: 2;

          then ( dist (p9,t)) <= (( dist (p9,q)) + ( dist (q,t))) & (( dist (p9,q)) + ( dist (q,t))) < ((r / 2) + (r / 2)) by A22, METRIC_1: 4, XREAL_1: 8;

          then ( dist (p9,t)) < r by XXREAL_0: 2;

          then t in ( Ball (p9,r)) by METRIC_1: 11;

          hence thesis by A14;

        end;

        Up is Basis of TM by A10, YELLOW_9: 32;

        then

         A23: ( weight TM) c= ( card Up) by WAYBEL23: 73;

        

         A24: ( card ( dom P)) = omega by CARD_1: 47, FUNCT_2:def 1;

        for x be object st x in ( dom P) holds ( card (P . x)) c= ( card Am)

        proof

          let x be object;

          assume

           A25: x in ( dom P);

          then P[x, (P . x)] by A9;

          hence thesis by A25;

        end;

        then ( card ( Union P)) c= ( omega *` ( card Am)) by A24, CARD_2: 86;

        hence thesis by A23;

      end;

    end;

    

     Lm7: ( density TM) c= iC implies ( weight TM) c= iC

    proof

      consider A be Subset of TM such that

       A1: A is dense and

       A2: ( density TM) = ( card A) by TOPGEN_1:def 12;

      

       A3: ( weight TM) c= ( omega *` ( card A)) by A1, Th17;

      assume ( density TM) c= iC;

      then ( omega *` ( card A)) c= ( omega *` iC) by A2, CARD_2: 90;

      then ( weight TM) c= ( omega *` iC) by A3;

      hence thesis by Lm5;

    end;

    begin

    theorem :: METRIZTS:18

    

     Th18: ( weight TM) c= iC iff for Fm st Fm is open & Fm is Cover of TM holds ex Gm st Gm c= Fm & Gm is Cover of TM & ( card Gm) c= iC

    proof

      hereby

        assume

         A1: ( weight TM) c= iC;

        let F be Subset-Family of TM such that

         A2: F is open and

         A3: F is Cover of TM;

        per cases ;

          suppose

           A4: TM is empty;

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

          take G;

          the carrier of TM = {} by A4;

          then ( [#] TM) = ( union G);

          hence G c= F & G is Cover of TM & ( card G) c= iC by SETFAM_1:def 11;

        end;

          suppose TM is non empty;

          then

          consider G be open Subset-Family of TM such that

           A5: G c= F & ( union G) = ( union F) & ( card G) c= ( weight TM) by A2, TOPGEN_2: 11;

          reconsider G as Subset-Family of TM;

          take G;

          ( union F) = ( [#] TM) by A3, SETFAM_1: 45;

          hence G c= F & G is Cover of TM & ( card G) c= iC by A1, A5, SETFAM_1:def 11;

        end;

      end;

      assume for F be Subset-Family of TM st F is open & F is Cover of TM holds ex G be Subset-Family of TM st G c= F & G is Cover of TM & ( card G) c= iC;

      then for A be Subset of TM st A is closed & A is discrete holds ( card A) c= iC by Th13;

      then for A be Subset of TM st A is discrete holds ( card A) c= iC by Th14;

      then for F be Subset-Family of TM st F is open & not {} in F & for A,B be Subset of TM st A in F & B in F & A <> B holds A misses B holds ( card F) c= iC by Th15;

      then ( density TM) c= iC by Lm6;

      hence thesis by Lm7;

    end;

    theorem :: METRIZTS:19

    

     Th19: ( weight TM) c= iC iff for Am st Am is closed & Am is discrete holds ( card Am) c= iC

    proof

      hereby

        assume ( weight TM) c= iC;

        then for Fm st Fm is open & Fm is Cover of TM holds ex Gm st Gm c= Fm & Gm is Cover of TM & ( card Gm) c= iC by Th18;

        hence for Am st Am is closed & Am is discrete holds ( card Am) c= iC by Th13;

      end;

      assume for Am st Am is closed & Am is discrete holds ( card Am) c= iC;

      then for Am st Am is discrete holds ( card Am) c= iC by Th14;

      then for Fm st Fm is open & not {} in Fm & for Am, Bm st Am in Fm & Bm in Fm & Am <> Bm holds Am misses Bm holds ( card Fm) c= iC by Th15;

      then ( density TM) c= iC by Lm6;

      hence thesis by Lm7;

    end;

    theorem :: METRIZTS:20

    

     Th20: ( weight TM) c= iC iff for Am st Am is discrete holds ( card Am) c= iC

    proof

      hereby

        assume ( weight TM) c= iC;

        then for A be Subset of TM st A is closed & A is discrete holds ( card A) c= iC by Th19;

        hence for A be Subset of TM st A is discrete holds ( card A) c= iC by Th14;

      end;

      assume for A be Subset of TM st A is discrete holds ( card A) c= iC;

      then for F be Subset-Family of TM st F is open & not {} in F & for A,B be Subset of TM st A in F & B in F & A <> B holds A misses B holds ( card F) c= iC by Th15;

      then ( density TM) c= iC by Lm6;

      hence thesis by Lm7;

    end;

    theorem :: METRIZTS:21

    

     Th21: ( weight TM) c= iC iff for Fm st Fm is open & not {} in Fm & for Am, Bm st Am in Fm & Bm in Fm & Am <> Bm holds Am misses Bm holds ( card Fm) c= iC

    proof

      hereby

        assume ( weight TM) c= iC;

        then for A be Subset of TM st A is discrete holds ( card A) c= iC by Th20;

        hence for F be Subset-Family of TM st F is open & not {} in F & for A,B be Subset of TM st A in F & B in F & A <> B holds A misses B holds ( card F) c= iC by Th15;

      end;

      assume for F be Subset-Family of TM st F is open & not {} in F & for A,B be Subset of TM st A in F & B in F & A <> B holds A misses B holds ( card F) c= iC;

      then ( density TM) c= iC by Lm6;

      hence thesis by Lm7;

    end;

    theorem :: METRIZTS:22

    

     Th22: ( weight TM) c= iC iff ( density TM) c= iC

    proof

      consider A be Subset of TM such that

       A1: A is dense and

       A2: ( density TM) = ( card A) by TOPGEN_1:def 12;

      hereby

        assume ( weight TM) c= iC;

        then for F be Subset-Family of TM st F is open & not {} in F & for A,B be Subset of TM st A in F & B in F & A <> B holds A misses B holds ( card F) c= iC by Th21;

        hence ( density TM) c= iC by Lm6;

      end;

      

       A3: ( weight TM) c= ( omega *` ( card A)) by A1, Th17;

      assume ( density TM) c= iC;

      then ( omega *` ( card A)) c= ( omega *` iC) by A2, CARD_2: 90;

      then ( weight TM) c= ( omega *` iC) by A3;

      hence thesis by Lm5;

    end;

    theorem :: METRIZTS:23

    

     Th23: for B be Basis of TM st for Fm st Fm is open & Fm is Cover of TM holds ex Gm st Gm c= Fm & Gm is Cover of TM & ( card Gm) c= iC holds ex underB be Basis of TM st underB c= B & ( card underB) c= iC

    proof

      let B be Basis of TM such that

       A1: for F be Subset-Family of TM st F is open & F is Cover of TM holds ex G be Subset-Family of TM st G c= F & G is Cover of TM & ( card G) c= iC;

      per cases ;

        suppose TM is empty;

        then ( weight TM) = 0 ;

        then

        consider underB be Basis of TM such that

         A2: ( card underB) = 0 by WAYBEL23: 74;

        take underB;

        underB = {} by A2;

        hence thesis;

      end;

        suppose

         A3: TM is non empty;

        set TOP = the topology of TM, cT = the carrier of TM;

        consider metr be Function of [:cT, cT:], REAL such that

         A4: metr is_metric_of cT and

         A5: ( Family_open_set ( SpaceMetr (cT,metr))) = TOP by PCOMPS_1:def 8;

        reconsider Tm = ( SpaceMetr (cT,metr)) as non empty MetrSpace by A3, A4, PCOMPS_1: 36;

        defpred P[ object, object] means for n be Nat st $1 = n holds ex G be open Subset-Family of TM st G c= { U where U be Subset of TM : U in B & ex p be Point of Tm st U c= ( Ball (p,(1 / (2 |^ n)))) } & G is Cover of TM & ( card G) c= iC & $2 = G;

        

         A6: B c= TOP by TOPS_2: 64;

        

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

        proof

          let x be object;

          assume x in NAT ;

          then

          reconsider n = x as Nat;

          set F = { U where U be Subset of TM : U in B & ex p be Element of Tm st U c= ( Ball (p,(1 / (2 |^ n)))) };

          

           A8: F c= TOP

          proof

            let f be object;

            assume f in F;

            then ex U be Subset of TM st f = U & U in B & ex p be Point of Tm st U c= ( Ball (p,(1 / (2 |^ n))));

            hence thesis by A6;

          end;

          then

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

          reconsider F as open Subset-Family of TM by A8, TOPS_2: 11;

          cT c= ( union F)

          proof

            let y be object;

            assume

             A9: y in cT;

            then

            reconsider p = y as Point of TM;

            reconsider q = y as Element of Tm by A3, A4, A9, PCOMPS_2: 4;

            (2 |^ n) > 0 & ( dist (q,q)) = 0 by METRIC_1: 1, NEWTON: 83;

            then

             A10: q in ( Ball (q,(1 / (2 |^ n)))) by METRIC_1: 11;

            reconsider BALL = ( Ball (q,(1 / (2 |^ n)))) as Subset of TM by A3, A4, PCOMPS_2: 4;

            BALL in ( Family_open_set Tm) by PCOMPS_1: 29;

            then BALL is open by A5;

            then

            consider U be Subset of TM such that

             A11: U in B and

             A12: p in U and

             A13: U c= BALL by A10, YELLOW_9: 31;

            U in F by A11, A13;

            hence thesis by A12, TARSKI:def 4;

          end;

          then F is Cover of TM by SETFAM_1:def 11;

          then

          consider G be Subset-Family of TM such that

           A14: G c= F and

           A15: G is Cover of TM & ( card G) c= iC by A1;

          take G;

          let m be Nat;

          assume

           A16: x = m;

          G is open by A14, TOPS_2: 11;

          hence thesis by A14, A15, A16;

        end;

        consider f be Function such that

         A17: ( dom f) = NAT & for e be object st e in NAT holds P[e, (f . e)] from CLASSES1:sch 1( A7);

        

         A18: ( union ( rng f)) c= B

        proof

          let b be object;

          assume b in ( union ( rng f));

          then

          consider y be set such that

           A19: b in y and

           A20: y in ( rng f) by TARSKI:def 4;

          consider x be object such that

           A21: x in ( dom f) and

           A22: (f . x) = y by A20, FUNCT_1:def 3;

          reconsider n = x as Nat by A17, A21;

          ex G be open Subset-Family of TM st G c= { U where U be Subset of TM : U in B & ex p be Point of Tm st U c= ( Ball (p,(1 / (2 |^ n)))) } & G is Cover of TM & ( card G) c= iC & (f . n) = G by A17, A21;

          then b in { U where U be Subset of TM : U in B & ex p be Point of Tm st U c= ( Ball (p,(1 / (2 |^ n)))) } by A19, A22;

          then ex U be Subset of TM st U = b & U in B & ex p be Point of Tm st U c= ( Ball (p,(1 / (2 |^ n))));

          hence thesis;

        end;

        then

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

        for A be Subset of TM st A is open holds for p be Point of TM st p in A holds ex a be Subset of TM st a in Urngf & p in a & a c= A

        proof

          let A be Subset of TM;

          assume A is open;

          then

           A23: A in ( Family_open_set Tm) by A5;

          let p be Point of TM such that

           A24: p in A;

          reconsider p9 = p as Element of Tm by A3, A4, PCOMPS_2: 4;

          consider r be Real such that

           A25: r > 0 and

           A26: ( Ball (p9,r)) c= A by A23, A24, PCOMPS_1:def 4;

          consider n be Nat such that

           A27: (1 / (2 |^ n)) <= (r / 2) by A25, PREPOWER: 92;

          

           A28: n in NAT by ORDINAL1:def 12;

          consider G be open Subset-Family of TM such that

           A29: G c= { U where U be Subset of TM : U in B & ex p be Point of Tm st U c= ( Ball (p,(1 / (2 |^ n)))) } and

           A30: G is Cover of TM and ( card G) c= iC and

           A31: (f . n) = G by A17, A28;

          ( [#] TM) = ( union G) by A30, SETFAM_1: 45;

          then

          consider a be set such that

           A32: p in a and

           A33: a in G by A3, TARSKI:def 4;

          a in { U where U be Subset of TM : U in B & ex p be Point of Tm st U c= ( Ball (p,(1 / (2 |^ n)))) } by A29, A33;

          then

          consider U be Subset of TM such that

           A34: a = U and U in B and

           A35: ex p be Point of Tm st U c= ( Ball (p,(1 / (2 |^ n))));

          take U;

          (f . n) in ( rng f) by A17, FUNCT_1:def 3, A28;

          hence U in Urngf & p in U by A31, A32, A33, A34, TARSKI:def 4;

          thus U c= A

          proof

            let u9 be object;

            consider pp be Element of Tm such that

             A36: U c= ( Ball (pp,(1 / (2 |^ n)))) by A35;

            assume

             A37: u9 in U;

            then

            reconsider u = u9 as Element of Tm by A3, A4, PCOMPS_2: 4;

            ( dist (pp,u)) < (1 / (2 |^ n)) by A36, A37, METRIC_1: 11;

            then

             A38: ( dist (pp,u)) < (r / 2) by A27, XXREAL_0: 2;

            ( dist (pp,p9)) < (1 / (2 |^ n)) by A32, A34, A36, METRIC_1: 11;

            then ( dist (p9,pp)) < (r / 2) by A27, XXREAL_0: 2;

            then ( dist (p9,u)) <= (( dist (p9,pp)) + ( dist (pp,u))) & (( dist (p9,pp)) + ( dist (pp,u))) < ((r / 2) + (r / 2)) by A38, METRIC_1: 4, XREAL_1: 8;

            then ( dist (p9,u)) < ((r / 2) + (r / 2)) by XXREAL_0: 2;

            then u in ( Ball (p9,r)) by METRIC_1: 11;

            hence thesis by A26;

          end;

        end;

        then

        reconsider Urngf as Basis of TM by A6, A18, XBOOLE_1: 1, YELLOW_9: 32;

        take Urngf;

        for x be object st x in ( dom f) holds ( card (f . x)) c= iC

        proof

          let x be object;

          assume x in ( dom f);

          then

          reconsider n = x as Element of NAT by A17;

          ex G be open Subset-Family of TM st G c= { U where U be Subset of TM : U in B & ex p be Point of Tm st U c= ( Ball (p,(1 / (2 |^ n)))) } & G is Cover of TM & ( card G) c= iC & (f . n) = G by A17;

          hence thesis;

        end;

        then ( card ( Union f)) c= ( omega *` iC) by A17, CARD_1: 47, CARD_2: 86;

        hence thesis by A18, Lm5;

      end;

    end;

    begin

    definition

      let T;

      :: METRIZTS:def2

      attr T is Lindelof means

      : Def2: for F st F is open & F is Cover of T holds ex G st G c= F & G is Cover of T & G is countable;

    end

    

     Lm8: T is Lindelof iff for F st F is open & F is Cover of T holds ex G st G c= F & G is Cover of T & ( card G) c= omega

    proof

      hereby

        assume

         A1: T is Lindelof;

        let F;

        assume F is open & F is Cover of T;

        then

        consider G be Subset-Family of T such that

         A2: G c= F & G is Cover of T & G is countable by A1;

        take G;

        thus G c= F & G is Cover of T & ( card G) c= omega by A2;

      end;

      assume

       A3: for F st F is open & F is Cover of T holds ex G st G c= F & G is Cover of T & ( card G) c= omega ;

      let F;

      assume F is open & F is Cover of T;

      then

      consider G such that

       A4: G c= F & G is Cover of T and

       A5: ( card G) c= omega by A3;

      G is countable by A5;

      hence thesis by A4;

    end;

    theorem :: METRIZTS:24

    for B be Basis of TM st TM is Lindelof holds ex B9 be Basis of TM st B9 c= B & B9 is countable

    proof

      let B be Basis of TM;

      assume TM is Lindelof;

      then for F be Subset-Family of TM st F is open & F is Cover of TM holds ex G be Subset-Family of TM st G c= F & G is Cover of TM & ( card G) c= omega by Lm8;

      then

      consider underB be Basis of TM such that

       A1: underB c= B & ( card underB) c= omega by Th23;

      take underB;

      thus thesis by A1;

    end;

    

     Lm9: TM is Lindelof iff TM is second-countable

    proof

      hereby

        assume TM is Lindelof;

        then for F be Subset-Family of TM st F is open & F is Cover of TM holds ex G be Subset-Family of TM st G c= F & G is Cover of TM & ( card G) c= omega by Lm8;

        then ( weight TM) c= omega by Th18;

        hence TM is second-countable by WAYBEL23:def 6;

      end;

      assume TM is second-countable;

      then ( weight TM) c= omega by WAYBEL23:def 6;

      then for F be Subset-Family of TM st F is open & F is Cover of TM holds ex G be Subset-Family of TM st G c= F & G is Cover of TM & ( card G) c= omega by Th18;

      hence thesis by Lm8;

    end;

    registration

      cluster Lindelof -> second-countable for metrizable TopSpace;

      coherence by Lm9;

    end

    

     Lm10: TM is Lindelof iff TM is separable

    proof

      hereby

        assume TM is Lindelof;

        then ( weight TM) c= omega by WAYBEL23:def 6;

        then ( density TM) c= omega by Th22;

        hence TM is separable by TOPGEN_1:def 13;

      end;

      assume TM is separable;

      then ( density TM) c= omega by TOPGEN_1:def 13;

      then ( weight TM) c= omega by Th22;

      then TM is second-countable by WAYBEL23:def 6;

      hence thesis by Lm9;

    end;

    registration

      cluster Lindelof -> separable for metrizable TopSpace;

      coherence by Lm10;

      cluster separable -> Lindelof for metrizable TopSpace;

      coherence by Lm10;

    end

    registration

      cluster Lindelof metrizable for non empty TopSpace;

      existence

      proof

        set X = the non empty finite set;

        ( TopSpaceMetr ( DiscreteSpace X)) is finite;

        hence thesis;

      end;

      cluster second-countable -> Lindelof for TopSpace;

      coherence

      proof

        let T be TopSpace;

        assume

         A1: T is second-countable;

        let F be Subset-Family of T such that

         A2: F is open and

         A3: F is Cover of T;

        per cases ;

          suppose

           A4: T is empty;

          take F;

          F c= { {} }

          proof

            let x be object;

            assume x in F;

            then x = {} by A4;

            hence thesis by TARSKI:def 1;

          end;

          hence thesis by A3;

        end;

          suppose T is non empty;

          hence thesis by A1, A2, A3, COMPL_SP: 34;

        end;

      end;

      cluster regular Lindelof -> normal for TopSpace;

      coherence

      proof

        let T be TopSpace;

        assume that

         A5: T is regular and

         A6: T is Lindelof;

        per cases ;

          suppose

           A7: T is empty;

          let F1,F2 be Subset of T such that F1 is closed and F2 is closed and

           A8: F1 misses F2;

          take F1, F2;

          thus thesis by A7, A8;

        end;

          suppose

           A9: T is non empty;

          set TOP = the topology of T;

          for A be Subset of T, U be open Subset of T st A is closed & U is open & A c= U holds ex W be sequence of ( bool the carrier of T) st A c= ( Union W) & ( Union W) c= U & for n be Element of NAT holds ( Cl (W . n)) c= U & (W . n) is open

          proof

            let A be Subset of T, U be open Subset of T such that

             A10: A is closed and U is open and

             A11: A c= U;

            defpred P[ object, object] means for p be Point of T st p = $1 holds ex W be Subset of T st W is open & p in W & ( Cl W) c= U & $2 = W;

            

             A12: for x be object st x in A holds ex y be object st y in TOP & P[x, y]

            proof

              let x be object;

              assume

               A13: x in A;

              then

              reconsider p = x as Point of T;

              U = ((U ` ) ` );

              then

              consider G1,G2 be Subset of T such that

               A14: G1 is open and

               A15: G2 is open and

               A16: p in G1 and

               A17: (U ` ) c= G2 and

               A18: G1 misses G2 by A5, A11, A13;

              

               A19: ( Cl (G2 ` )) = (G2 ` ) & (G2 ` ) c= U by A15, A17, PRE_TOPC: 22, SUBSET_1: 17;

              take G1;

              thus G1 in TOP by A14;

              G1 c= (G2 ` ) by A18, SUBSET_1: 23;

              then

               A20: ( Cl G1) c= ( Cl (G2 ` )) by PRE_TOPC: 19;

              let q be Point of T;

              assume q = x;

              hence thesis by A14, A16, A20, A19, XBOOLE_1: 1;

            end;

            consider w be Function of A, TOP such that

             A21: for x be object st x in A holds P[x, (w . x)] from FUNCT_2:sch 1( A12);

            (A ` ) in TOP by A10, PRE_TOPC:def 2;

            then TOP is open & {(A ` )} c= TOP by ZFMISC_1: 31;

            then

            reconsider RNG = ( rng w), AA = {(A ` )} as open Subset-Family of T by TOPS_2: 11, XBOOLE_1: 1;

            set RngA = (RNG \/ AA);

            

             A22: ( dom w) = A by FUNCT_2:def 1;

            ( [#] T) c= ( union RngA)

            proof

              let x be object;

              assume

               A23: x in ( [#] T);

              per cases ;

                suppose

                 A24: x in A;

                then

                consider W be Subset of T such that W is open and

                 A25: x in W and ( Cl W) c= U and

                 A26: (w . x) = W by A21;

                W in ( rng w) by A22, A24, A26, FUNCT_1:def 3;

                then W in RngA by XBOOLE_0:def 3;

                hence thesis by A25, TARSKI:def 4;

              end;

                suppose

                 A27: not x in A;

                (A ` ) in AA by TARSKI:def 1;

                then

                 A28: (A ` ) in RngA by XBOOLE_0:def 3;

                x in (A ` ) by A23, A27, XBOOLE_0:def 5;

                hence thesis by A28, TARSKI:def 4;

              end;

            end;

            then RngA is open Subset-Family of T & RngA is Cover of T by SETFAM_1:def 11, TOPS_2: 13;

            then

            consider G be Subset-Family of T such that

             A29: G c= RngA and

             A30: G is Cover of T and

             A31: G is countable by A6;

            

             A32: ( [#] T) = ( union G) by A30, SETFAM_1: 45;

            per cases ;

              suppose (G \ AA) is empty;

              then G c= AA by XBOOLE_1: 37;

              then

               A33: ( union G) c= ( union AA) by ZFMISC_1: 77;

              take W = ( NAT --> ( {} T));

              ( rng W) = {( {} T)} by FUNCOP_1: 8;

              then

               A34: (( {} T) ` ) = ( [#] T) & ( Union W) = ( {} T) by ZFMISC_1: 25;

              ( union AA) = (A ` ) by ZFMISC_1: 25;

              then (A ` ) = ( [#] T) by A32, A33;

              hence A c= ( Union W) & ( Union W) c= U by A34, SUBSET_1: 42;

              let n be Element of NAT ;

              (W . n) = ( {} T) by FUNCOP_1: 7;

              then ( Cl (W . n)) = ( {} T) by PRE_TOPC: 22;

              hence thesis by FUNCOP_1: 7;

            end;

              suppose

               A35: (G \ AA) is non empty;

              (G \ AA) is countable by A31, CARD_3: 95;

              then

              consider W be sequence of (G \ AA) such that

               A36: ( rng W) = (G \ AA) by A35, CARD_3: 96;

              reconsider W as sequence of ( bool the carrier of T) by A35, A36, FUNCT_2: 6;

              take W;

              thus A c= ( Union W)

              proof

                let x be object;

                assume

                 A37: x in A;

                then

                consider y be set such that

                 A38: x in y and

                 A39: y in G by A32, TARSKI:def 4;

                 not x in (A ` ) by A37, XBOOLE_0:def 5;

                then not y in AA by A38, TARSKI:def 1;

                then y in ( rng W) by A36, A39, XBOOLE_0:def 5;

                then ex n be object st n in ( dom W) & (W . n) = y by FUNCT_1:def 3;

                hence thesis by A38, PROB_1: 12;

              end;

              

               A40: ( dom W) = NAT by FUNCT_2:def 1;

              thus ( Union W) c= U

              proof

                let x be object;

                assume x in ( Union W);

                then

                consider n be Nat such that

                 A41: x in (W . n) by PROB_1: 12;

                

                 A42: n in NAT by ORDINAL1:def 12;

                

                 A43: (W . n) in (G \ AA) by A36, A40, FUNCT_1:def 3, A42;

                then (W . n) in G by ZFMISC_1: 56;

                then

                 A44: (W . n) in RNG or (W . n) in AA by A29, XBOOLE_0:def 3;

                (W . n) <> (A ` ) by A43, ZFMISC_1: 56;

                then

                consider xx be object such that

                 A45: xx in ( dom w) & (w . xx) = (W . n) by A44, FUNCT_1:def 3, TARSKI:def 1;

                consider W9 be Subset of T such that W9 is open and xx in W9 and

                 A46: ( Cl W9) c= U and

                 A47: (W . n) = W9 by A21, A22, A45;

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

                then x in ( Cl W9) by A41, A47;

                hence thesis by A46;

              end;

              let n be Element of NAT ;

              

               A48: (W . n) in (G \ AA) by A36, A40, FUNCT_1:def 3;

              then (W . n) in G by ZFMISC_1: 56;

              then

               A49: (W . n) in RNG or (W . n) in AA by A29, XBOOLE_0:def 3;

              (W . n) <> (A ` ) by A48, ZFMISC_1: 56;

              then

              consider xx be object such that

               A50: xx in ( dom w) & (w . xx) = (W . n) by A49, FUNCT_1:def 3, TARSKI:def 1;

              ex W9 be Subset of T st W9 is open & xx in W9 & ( Cl W9) c= U & (W . n) = W9 by A21, A22, A50;

              hence thesis;

            end;

          end;

          hence thesis by A9, NAGATA_1: 18;

        end;

      end;

      cluster countable -> Lindelof for TopSpace;

      coherence

      proof

        let T be TopSpace;

        assume T is countable;

        then ( [#] T) is countable by ORDERS_4:def 2;

        then

         A51: ( card ( [#] T)) c= omega ;

        let F be Subset-Family of T;

        assume that F is open and

         A52: F is Cover of T;

        consider G be Subset-Family of T such that

         A53: G c= F & G is Cover of T and

         A54: ( card G) c= ( card ( [#] T)) by A52, Th16;

        take G;

        ( card G) c= omega by A51, A54;

        hence thesis by A53;

      end;

    end

    

     Lm11: the TopStruct of ( TOP-REAL 1) is second-countable

    proof

      reconsider R = RAT as Subset of R^1 by NUMBERS: 12, TOPMETR: 17;

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

      then

       A1: ( weight [: the TopStruct of ( TOP-REAL 1), the TopStruct of ( TOP-REAL 1):]) = ( weight the TopStruct of ( TOP-REAL 2)) by Th4, TOPREAL7: 25;

      ( Cl R) = ( [#] R^1 ) by BORSUK_5: 15;

      then R is dense by TOPS_1:def 3;

      then R^1 is separable by TOPGEN_4: 6;

      then

       A2: ( weight [: R^1 , R^1 :]) c= omega by TOPMETR:def 6, WAYBEL23:def 6;

      ( the TopStruct of [: R^1 , R^1 :], the TopStruct of ( TOP-REAL 2)) are_homeomorphic by TOPREAL6: 77, TOPREALA: 15;

      then

       A3: ( weight the TopStruct of [: R^1 , R^1 :]) = ( weight the TopStruct of ( TOP-REAL 2)) by Th4;

      ( weight the TopStruct of ( TOP-REAL 1)) c= ( weight [: the TopStruct of ( TOP-REAL 1), the TopStruct of ( TOP-REAL 1):]) by Th6;

      then ( weight the TopStruct of ( TOP-REAL 1)) c= omega by A1, A3, A2;

      hence thesis by WAYBEL23:def 6;

    end;

    registration

      let n be Nat;

      cluster the TopStruct of ( TOP-REAL n) -> second-countable;

      coherence

      proof

        defpred P[ Nat] means the TopStruct of ( TOP-REAL $1) is second-countable;

        

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

        proof

          let n be Nat;

          

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

          assume P[n];

          then

           A3: ( weight [: the TopStruct of ( TOP-REAL n), the TopStruct of ( TOP-REAL 1):]) c= omega by Lm11, WAYBEL23:def 6;

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

          then ( weight [: the TopStruct of ( TOP-REAL n), the TopStruct of ( TOP-REAL 1):]) = ( weight the TopStruct of ( TOP-REAL (n + 1))) by A2, Th4, TOPREAL7: 25;

          hence thesis by A3, WAYBEL23:def 6;

        end;

        ( [#] ( TOP-REAL 0 )) = ( REAL 0 ) by EUCLID: 22

        .= ( 0 -tuples_on REAL ) by EUCLID:def 1

        .= {( <*> REAL )} by FINSEQ_2: 94;

        then the TopStruct of ( TOP-REAL 0 ) is finite;

        then

         A4: P[ 0 ];

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

        hence thesis;

      end;

    end

    registration

      let T be Lindelof TopSpace;

      let A be closed Subset of T;

      cluster (T | A) -> Lindelof;

      coherence

      proof

        reconsider E = { {} } as Subset-Family of (T | A) by SETFAM_1: 46;

        defpred P[ object, object] means ex D2 be set st D2 = $2 & (D2 /\ A) = $1;

        set TOP = the topology of T;

        let FA be Subset-Family of (T | A) such that

         A1: FA is open and

         A2: FA is Cover of (T | A);

        

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

        proof

          let x be object such that

           A4: x in FA;

          reconsider X = x as Subset of (T | A) by A4;

          X is open by A1, A4;

          then X in the topology of (T | A);

          then

          consider Q be Subset of T such that

           A5: Q in TOP & X = (Q /\ ( [#] (T | A))) by PRE_TOPC:def 4;

          take Q;

          thus Q in TOP by A5;

          take Q;

          thus thesis by A5, PRE_TOPC:def 5;

        end;

        consider f be Function of FA, TOP such that

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

        (A ` ) in TOP by PRE_TOPC:def 2;

        then TOP is open & {(A ` )} c= TOP by ZFMISC_1: 31;

        then

        reconsider RNG = ( rng f), AA = {(A ` )} as open Subset-Family of T by TOPS_2: 11, XBOOLE_1: 1;

        reconsider RA = (RNG \/ AA) as open Subset-Family of T by TOPS_2: 13;

        

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

        

         A8: ( dom f) = FA by FUNCT_2:def 1;

        ( [#] T) c= ( union RA)

        proof

          

           A9: (A \/ (A ` )) = ( [#] the carrier of T) by SUBSET_1: 10;

          let x be object such that

           A10: x in ( [#] T);

          per cases by A9, A10, XBOOLE_0:def 3;

            suppose

             A11: x in A;

            A = ( union FA) by A2, A7, SETFAM_1: 45;

            then

            consider y be set such that

             A12: x in y and

             A13: y in FA by A11, TARSKI:def 4;

            (f . y) in RNG by A8, A13, FUNCT_1:def 3;

            then

             A14: (f . y) in RA by XBOOLE_0:def 3;

             P[y, (f . y)] by A6, A13;

            then ((f . y) /\ A) = y;

            then x in (f . y) by A12, XBOOLE_0:def 4;

            hence thesis by A14, TARSKI:def 4;

          end;

            suppose

             A15: x in (A ` );

            (A ` ) in AA by TARSKI:def 1;

            then (A ` ) in RA by XBOOLE_0:def 3;

            hence thesis by A15, TARSKI:def 4;

          end;

        end;

        then RA is Cover of T by SETFAM_1:def 11;

        then

        consider G be Subset-Family of T such that

         A16: G c= RA and

         A17: G is Cover of T and

         A18: G is countable by Def2;

        set GA = (G | A);

        take GE = (GA \ E);

        thus GE c= FA

        proof

          let x be object;

          assume

           A19: x in GE;

          then

           A20: x <> {} by ZFMISC_1: 56;

          x in GA by A19, ZFMISC_1: 56;

          then

          consider R be Subset of T such that

           A21: R in G and

           A22: (R /\ A) = x by TOPS_2:def 3;

          per cases by A16, A21, XBOOLE_0:def 3;

            suppose R in RNG;

            then

            consider y be object such that

             A23: y in ( dom f) and

             A24: (f . y) = R by FUNCT_1:def 3;

             P[y, (f . y)] by A6, A23;

            then y = (R /\ A) by A24;

            hence thesis by A22, A23;

          end;

            suppose R in AA;

            then R = (A ` ) by TARSKI:def 1;

            then x = (A \ A) by A22, SUBSET_1: 13;

            hence thesis by A20, XBOOLE_1: 37;

          end;

        end;

        ( union G) = ( [#] T) by A17, SETFAM_1: 45;

        

        then ( [#] (T | A)) = ( union GA) by A7, TOPS_2: 33

        .= ( union GE) by PARTIT1: 2;

        hence GE is Cover of (T | A) by SETFAM_1:def 11;

        

         A25: ( card GA) c= ( card G) by Th7;

        ( card G) c= omega by A18;

        then ( card GA) c= omega by A25;

        then GA is countable;

        hence thesis by CARD_3: 95;

      end;

    end

    registration

      let TM be Lindelof metrizable TopSpace;

      let A be Subset of TM;

      cluster (TM | A) -> Lindelof;

      coherence ;

    end

    definition

      let T;

      let A,B,L be Subset of T;

      :: METRIZTS:def3

      pred L separates A,B means ex U,W be open Subset of T st A c= U & B c= W & U misses W & L = ((U \/ W) ` );

    end

    

     Lm12: for M be non empty MetrSpace holds for A,B be non empty Subset of ( TopSpaceMetr M) holds { p where p be Point of ( TopSpaceMetr M) : ((( dist_min A) . p) - (( dist_min B) . p)) < 0 } is open Subset of ( TopSpaceMetr M)

    proof

      let M be non empty MetrSpace;

      set TM = ( TopSpaceMetr M);

      let A,B be non empty Subset of TM;

      set dA = ( dist_min A);

      set dB = ( dist_min B);

      consider g be Function of the carrier of TM, the carrier of R^1 such that

       A1: for p be Point of TM, r1,r2 be Real st (dA . p) = r1 & (dB . p) = r2 holds (g . p) = (r1 - r2) and

       A2: g is continuous by JGRAPH_2: 21;

      set gA = { p where p be Point of TM : ((dA . p) - (dB . p)) < 0 };

      reconsider A = ]. -infty , 0 .[ as Subset of R^1 by TOPMETR: 17;

      

       A3: A is open by BORSUK_5: 40;

      

       A4: (g " A) c= gA

      proof

        let x be object;

        assume

         A5: x in (g " A);

        then

        reconsider p = x as Point of TM;

        

         A6: (g . x) in A by A5, FUNCT_1:def 7;

        ((dA . p) - (dB . p)) = (g . x) by A1;

        then ((dA . p) - (dB . p)) < 0 by A6, XXREAL_1: 233;

        hence thesis;

      end;

      

       A7: gA c= (g " A)

      proof

        let x be object;

        assume x in gA;

        then

        consider p be Point of TM such that

         A8: p = x and

         A9: ((dA . p) - (dB . p)) < 0 ;

        (g . p) = ((dA . p) - (dB . p)) by A1;

        then ( dom g) = ( [#] TM) & (g . p) in A by A9, FUNCT_2:def 1, XXREAL_1: 233;

        hence thesis by A8, FUNCT_1:def 7;

      end;

      ( [#] R^1 ) = {} implies ( [#] TM) = {} ;

      then (g " A) is open by A2, A3, TOPS_2: 43;

      hence thesis by A4, A7, XBOOLE_0:def 10;

    end;

    

     Lm13: for A,B be Subset of TM st (A,B) are_separated holds ex U,W be open Subset of TM st A c= U & B c= W & U misses W

    proof

      let A,B be Subset of TM such that

       A1: (A,B) are_separated ;

      set TOP = the topology of TM, cTM = the carrier of TM;

      consider metr be Function of [:cTM, cTM:], REAL such that

       A2: metr is_metric_of cTM and

       A3: ( Family_open_set ( SpaceMetr (cTM,metr))) = TOP by PCOMPS_1:def 8;

      per cases ;

        suppose

         A4: A = ( {} TM);

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

        thus thesis by A4;

      end;

        suppose

         A5: B = ( {} TM);

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

        thus thesis by A5;

      end;

        suppose

         A6: A <> ( {} TM) & B <> ( {} TM);

        then

         A7: TM is non empty;

        then

        reconsider Tm = ( SpaceMetr (cTM,metr)) as non empty MetrSpace by A2, PCOMPS_1: 36;

        set TTm = ( TopSpaceMetr Tm);

        reconsider A9 = A, B9 = B as Subset of TTm by A2, A7, PCOMPS_2: 4;

        set dA = ( dist_min A9), dB = ( dist_min B9);

        reconsider U = { p where p be Point of Tm : ((dA . p) - (dB . p)) < 0 }, W = { p where p be Point of Tm : ((dB . p) - (dA . p)) < 0 } as open Subset of TTm by A6, Lm12;

        U in ( Family_open_set Tm) & W in ( Family_open_set Tm) by PRE_TOPC:def 2;

        then

        reconsider U, W as open Subset of TM by A3, PRE_TOPC:def 2;

        take U, W;

        

         A8: ( [#] TM) = ( [#] TTm) by A2, A7, PCOMPS_2: 4;

        thus A c= U

        proof

          let x be object;

          assume

           A9: x in A;

          then

          reconsider p = x as Point of Tm by A2, A7, PCOMPS_2: 4;

          A misses ( Cl B) by A1, CONNSP_1:def 1;

          then not x in ( Cl B) by A9, XBOOLE_0: 3;

          then not x in ( Cl B9) by A3, A8, TOPS_3: 80;

          then

           A10: (dB . p) <> 0 by A6, HAUSDORF: 8;

          

           A11: (dB . p) >= 0 by A6, JORDAN1K: 9;

          (dA . p) = 0 by A9, HAUSDORF: 5;

          then ((dA . p) - (dB . p)) < 0 by A10, A11;

          hence thesis;

        end;

        thus B c= W

        proof

          let x be object;

          assume

           A12: x in B;

          then

          reconsider p = x as Point of Tm by A2, A7, PCOMPS_2: 4;

          B misses ( Cl A) by A1, CONNSP_1:def 1;

          then not x in ( Cl A) by A12, XBOOLE_0: 3;

          then not x in ( Cl A9) by A3, A8, TOPS_3: 80;

          then

           A13: (dA . p) <> 0 by A6, HAUSDORF: 8;

          

           A14: (dA . p) >= 0 by A6, JORDAN1K: 9;

          (dB . p) = 0 by A12, HAUSDORF: 5;

          then ((dB . p) - (dA . p)) < 0 by A13, A14;

          hence thesis;

        end;

        thus U misses W

        proof

          assume U meets W;

          then

          consider x be object such that

           A15: x in U and

           A16: x in W by XBOOLE_0: 3;

          consider p be Point of Tm such that

           A17: p = x and

           A18: ((dB . p) - (dA . p)) < 0 by A16;

          ex q be Point of Tm st q = x & ((dA . q) - (dB . q)) < 0 by A15;

          then ( - ((dA . p) - (dB . p))) > ( - 0 ) by A17;

          hence thesis by A18;

        end;

      end;

    end;

    theorem :: METRIZTS:25

    (Am,Bm) are_separated implies ex L be Subset of TM st L separates (Am,Bm)

    proof

      assume (Am,Bm) are_separated ;

      then

      consider U,W be open Subset of TM such that

       A1: Am c= U & Bm c= W & U misses W by Lm13;

      take ((U \/ W) ` );

      thus thesis by A1;

    end;

    theorem :: METRIZTS:26

    for M be Subset of TM, A1,A2 be closed Subset of TM, V1,V2 be open Subset of TM st A1 c= V1 & A2 c= V2 & ( Cl V1) misses ( Cl V2) holds for mV1,mV2,mL be Subset of (TM | M) st mV1 = (M /\ ( Cl V1)) & mV2 = (M /\ ( Cl V2)) & mL separates (mV1,mV2) holds ex L be Subset of TM st L separates (A1,A2) & (M /\ L) c= mL

    proof

      let M be Subset of TM, A1,A2 be closed Subset of TM, V1,V2 be open Subset of TM such that

       A1: A1 c= V1 and

       A2: A2 c= V2 and

       A3: ( Cl V1) misses ( Cl V2);

      set TMM = (TM | M);

      let mV1,mV2,mL be Subset of TMM such that

       A4: mV1 = (M /\ ( Cl V1)) and

       A5: mV2 = (M /\ ( Cl V2)) and

       A6: mL separates (mV1,mV2);

      

       A7: (V2 /\ M) c= mV2 by A5, PRE_TOPC: 18, XBOOLE_1: 26;

      consider U9,W9 be open Subset of TMM such that

       A8: mV1 c= U9 and

       A9: mV2 c= W9 and

       A10: U9 misses W9 and

       A11: mL = ((U9 \/ W9) ` ) by A6;

      

       A12: ( [#] TMM) = M by PRE_TOPC:def 5;

      then

      reconsider u = U9, w = W9 as Subset of TM by XBOOLE_1: 1;

      set u1 = (u \/ A1), w1 = (w \/ A2);

      

       A13: (mV2 /\ u) c= (U9 /\ W9) by A9, XBOOLE_1: 26;

      (U9,W9) are_separated by A10, TSEP_1: 37;

      then

       A14: (u,w) are_separated by CONNSP_1: 5;

      (V2 /\ u) = (V2 /\ (M /\ u)) by A12, XBOOLE_1: 28

      .= ((V2 /\ M) /\ u) by XBOOLE_1: 16;

      then (V2 /\ u) c= (mV2 /\ u) by A7, XBOOLE_1: 26;

      then (V2 /\ u) c= (U9 /\ W9) by A13;

      then (V2 /\ u) c= {} by A10;

      then (V2 /\ u) = {} ;

      then V2 misses u;

      then

       A15: V2 misses ( Cl u) by TSEP_1: 36;

      

       A16: ( Cl u1) misses w1

      proof

        assume ( Cl u1) meets w1;

        then

        consider x be object such that

         A17: x in ( Cl u1) & x in w1 by XBOOLE_0: 3;

        

         A18: ( Cl u1) = (( Cl u) \/ ( Cl A1)) by PRE_TOPC: 20;

        per cases by A17, A18, XBOOLE_0:def 3;

          suppose x in ( Cl u) & x in w;

          then w meets ( Cl u) by XBOOLE_0: 3;

          hence contradiction by A14, CONNSP_1:def 1;

        end;

          suppose x in ( Cl u) & x in A2;

          hence contradiction by A2, A15, XBOOLE_0: 3;

        end;

          suppose

           A19: x in ( Cl A1) & x in w;

          ( Cl A1) c= ( Cl V1) by A1, PRE_TOPC: 19;

          then x in mV1 by A4, A12, A19, XBOOLE_0:def 4;

          hence contradiction by A8, A10, A19, XBOOLE_0: 3;

        end;

          suppose

           A20: x in ( Cl A1) & x in A2;

          

           A21: ( Cl A1) c= ( Cl V1) & V2 c= ( Cl V2) by A1, PRE_TOPC: 18, PRE_TOPC: 19;

          x in V2 by A2, A20;

          hence thesis by A3, A20, A21, XBOOLE_0: 3;

        end;

      end;

      

       A22: (V1 /\ M) c= mV1 by A4, PRE_TOPC: 18, XBOOLE_1: 26;

      

       A23: (mV1 /\ w) c= (U9 /\ W9) by A8, XBOOLE_1: 26;

      (V1 /\ w) = (V1 /\ (M /\ w)) by A12, XBOOLE_1: 28

      .= ((V1 /\ M) /\ w) by XBOOLE_1: 16;

      then (V1 /\ w) c= (mV1 /\ w) by A22, XBOOLE_1: 26;

      then (V1 /\ w) c= (U9 /\ W9) by A23;

      then (V1 /\ w) c= {} by A10;

      then (V1 /\ w) = {} ;

      then V1 misses w;

      then

       A24: V1 misses ( Cl w) by TSEP_1: 36;

      ( Cl w1) misses u1

      proof

        assume ( Cl w1) meets u1;

        then

        consider x be object such that

         A25: x in ( Cl w1) & x in u1 by XBOOLE_0: 3;

        

         A26: ( Cl w1) = (( Cl w) \/ ( Cl A2)) by PRE_TOPC: 20;

        per cases by A25, A26, XBOOLE_0:def 3;

          suppose x in ( Cl w) & x in u;

          then ( Cl w) meets u by XBOOLE_0: 3;

          hence contradiction by A14, CONNSP_1:def 1;

        end;

          suppose x in ( Cl w) & x in A1;

          hence contradiction by A1, A24, XBOOLE_0: 3;

        end;

          suppose

           A27: x in ( Cl A2) & x in u;

          ( Cl A2) c= ( Cl V2) by A2, PRE_TOPC: 19;

          then x in mV2 by A5, A12, A27, XBOOLE_0:def 4;

          hence contradiction by A9, A10, A27, XBOOLE_0: 3;

        end;

          suppose

           A28: x in ( Cl A2) & x in A1;

          

           A29: ( Cl A2) c= ( Cl V2) & V1 c= ( Cl V1) by A2, PRE_TOPC: 18, PRE_TOPC: 19;

          x in V1 by A1, A28;

          hence thesis by A3, A28, A29, XBOOLE_0: 3;

        end;

      end;

      then (u1,w1) are_separated by A16, CONNSP_1:def 1;

      then

      consider U1,W1 be open Subset of TM such that

       A30: u1 c= U1 and

       A31: w1 c= W1 and

       A32: U1 misses W1 by Lm13;

      take L = ((U1 \/ W1) ` );

      A2 c= w1 by XBOOLE_1: 7;

      then

       A33: A2 c= W1 by A31;

      w c= w1 by XBOOLE_1: 7;

      then

       A34: w c= W1 by A31;

      u c= u1 by XBOOLE_1: 7;

      then u c= U1 by A30;

      then

       A35: (u \/ w) c= (U1 \/ W1) by A34, XBOOLE_1: 13;

      A1 c= u1 by XBOOLE_1: 7;

      then A1 c= U1 by A30;

      hence L separates (A1,A2) by A32, A33;

      

       A36: (( [#] TMM) \ (U9 \/ W9)) = mL by A11;

      (M /\ L) = ((M /\ ( [#] TM)) \ (U1 \/ W1)) by XBOOLE_1: 49

      .= (M \ (U1 \/ W1)) by XBOOLE_1: 28;

      then (M /\ L) c= (M \ (U9 \/ W9)) by A35, XBOOLE_1: 34;

      hence thesis by A36, PRE_TOPC:def 5;

    end;