topgen_2.miz

    begin

    reserve a,b,c for set;

    theorem :: TOPGEN_2:1



     Th1: for T be non empty TopSpace, B be Basis of T holds for x be Element of T holds { U where U be Subset of T : x in U & U in B } is Basis of x

    proof

      let T be non empty TopSpace;

      let B be Basis of T;

      let x be Element of T;

      set Bx = { U where U be Subset of T : x in U & U in B };



       A1: Bx c= B

      proof

        let a be object;

        assume a in Bx;

        then ex U be Subset of T st a = U & x in U & U in B;

        hence thesis;

      end;

      then

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

      Bx is Basis of x

      proof

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

        then Bx c= the topology of T by A1;

        then

         A2: Bx is open by TOPS_2: 64;

        Bx is x -quasi_basis

        proof

          now

            let a;

            assume a in Bx;

            then ex U be Subset of T st a = U & x in U & U in B;

            hence x in a;

          end;

          hence x in ( Intersect Bx) by SETFAM_1: 43;

          let S be Subset of T such that

           A3: S is open and

           A4: x in S;

          consider V be Subset of T such that

           A5: V in B and

           A6: x in V and

           A7: V c= S by A3, A4, YELLOW_9: 31;

          V in Bx by A5, A6;

          hence thesis by A7;

        end;

        hence thesis by A2;

      end;

      hence thesis;

    end;

    theorem :: TOPGEN_2:2



     Th2: for T be non empty TopSpace holds for B be ManySortedSet of T st for x be Element of T holds (B . x) is Basis of x holds ( Union B) is Basis of T

    proof

      let T be non empty TopSpace;

      let B be ManySortedSet of T;

      assume

       A1: for x be Element of T holds (B . x) is Basis of x;

      ( Union B) c= ( bool the carrier of T)

      proof

        let a be object;

        assume a in ( Union B);

        then

        consider b be object such that

         A2: b in ( dom B) and

         A3: a in (B . b) by CARD_5: 2;

        reconsider b as Point of T by A2;

        (B . b) is Basis of b by A1;

        hence thesis by A3;

      end;

      then

      reconsider W = ( Union B) as Subset-Family of T;



       A4: ( dom B) = the carrier of T by PARTFUN1:def 2;

       A5:

      now

        let A be Subset of T such that

         A6: A is open;

        let p be Point of T such that

         A7: p in A;



         A8: (B . p) is Basis of p by A1;

        then

        consider a be Subset of T such that

         A9: a in (B . p) and

         A10: a c= A by A6, A7, YELLOW_8:def 1;

        take a;

        thus a in W by A4, A9, CARD_5: 2;

        thus p in a by A8, A9, YELLOW_8: 12;

        thus a c= A by A10;

      end;

      W c= the topology of T

      proof

        let a be object;

        assume a in W;

        then

        consider b be object such that

         A11: b in ( dom B) and

         A12: a in (B . b) by CARD_5: 2;

        reconsider b as Point of T by A11;

        (B . b) is Basis of b by A1;

        then (B . b) c= the topology of T by TOPS_2: 64;

        hence thesis by A12;

      end;

      hence thesis by A5, YELLOW_9: 32;

    end;

    definition

      let T be non empty TopStruct;

      let x be Element of T;

      :: TOPGEN_2:def1

      func Chi (x,T) -> cardinal number means

      : Def1: (ex B be Basis of x st it = ( card B)) & for B be Basis of x holds it c= ( card B);

      existence

      proof

        set B0 = the Basis of x;

        defpred P[ Ordinal] means ex B be Basis of x st $1 = ( card B);

        ( card B0) is ordinal;

        then

         A1: ex A be Ordinal st P[A];

        consider A be Ordinal such that

         A2: P[A] and

         A3: for B be Ordinal st P[B] holds A c= B from ORDINAL1:sch 1( A1);

        consider B1 be Basis of x such that

         A4: A = ( card B1) by A2;

        take ( card B1);

        thus thesis by A3, A4;

      end;

      uniqueness

      proof

        let M1,M2 be cardinal number;

        assume that

         A5: ex B be Basis of x st M1 = ( card B) and

         A6: for B be Basis of x holds M1 c= ( card B) and

         A7: ex B be Basis of x st M2 = ( card B) and

         A8: for B be Basis of x holds M2 c= ( card B);

        thus M1 c= M2 & M2 c= M1 by A5, A6, A7, A8;

      end;

    end

    theorem :: TOPGEN_2:3



     Th3: for X be set st for a be set st a in X holds a is cardinal number holds ( union X) is cardinal number

    proof

      let X be set such that

       A1: for a be set st a in X holds a is cardinal number;

      now

        let a;

        assume

         A2: a in X;

        then a is cardinal number by A1;

        hence ex b be set st b in X & a c= b & b is cardinal set by A2;

      end;

      hence thesis by CARD_LAR: 32;

    end;

     Lm1:

    now

      let T be non empty TopStruct;

      set X = the set of all ( Chi (x,T)) where x be Point of T;

      now

        let a;

        assume a in X;

        then ex x be Point of T st a = ( Chi (x,T));

        hence a is cardinal number;

      end;

      hence ( union X) is cardinal number by Th3;

      let m be cardinal number such that

       A1: m = ( union X);

      hereby

        let x be Point of T;

        ( Chi (x,T)) in X;

        hence ( Chi (x,T)) c= m by A1, ZFMISC_1: 74;

      end;

      let M be cardinal number such that

       A2: for x be Point of T holds ( Chi (x,T)) c= M;

      now

        let a;

        assume a in X;

        then ex x be Point of T st a = ( Chi (x,T));

        hence a c= M by A2;

      end;

      hence m c= M by A1, ZFMISC_1: 76;

    end;

    definition

      let T be non empty TopStruct;

      :: TOPGEN_2:def2

      func Chi (T) -> cardinal number means

      : Def2: (for x be Point of T holds ( Chi (x,T)) c= it ) & for M be cardinal number st for x be Point of T holds ( Chi (x,T)) c= M holds it c= M;

      existence

      proof

        set X = the set of all ( Chi (x,T)) where x be Point of T;

        reconsider m = ( union X) as cardinal number by Lm1;

        take m;

        thus thesis by Lm1;

      end;

      uniqueness

      proof

        let M1,M2 be cardinal number;

        assume that

         A1: for x be Point of T holds ( Chi (x,T)) c= M1 and

         A2: for M be cardinal number st for x be Point of T holds ( Chi (x,T)) c= M holds M1 c= M and

         A3: for x be Point of T holds ( Chi (x,T)) c= M2 and

         A4: for M be cardinal number st for x be Point of T holds ( Chi (x,T)) c= M holds M2 c= M;

        thus M1 c= M2 & M2 c= M1 by A1, A2, A3, A4;

      end;

    end

    theorem :: TOPGEN_2:4



     Th4: for T be non empty TopStruct holds ( Chi T) = ( union the set of all ( Chi (x,T)) where x be Point of T)

    proof

      let T be non empty TopStruct;

      set X = the set of all ( Chi (x,T)) where x be Point of T;

      reconsider m = ( union X) as cardinal number by Lm1;



       A1: for M be cardinal number st for x be Point of T holds ( Chi (x,T)) c= M holds m c= M by Lm1;

      for x be Point of T holds ( Chi (x,T)) c= m by Lm1;

      hence thesis by A1, Def2;

    end;

    theorem :: TOPGEN_2:5



     Th5: for T be non empty TopStruct holds for x be Point of T holds ( Chi (x,T)) c= ( Chi T)

    proof

      let T be non empty TopStruct;

      set X = the set of all ( Chi (x,T)) where x be Point of T;

      let x be Point of T;



       A1: ( Chi (x,T)) in X;

      ( Chi T) = ( union X) by Th4;

      hence thesis by A1, ZFMISC_1: 74;

    end;

    theorem :: TOPGEN_2:6

    for T be non empty TopSpace holds T is first-countable iff ( Chi T) c= omega

    proof

      let T be non empty TopSpace;

      set X = the set of all ( Chi (x,T)) where x be Point of T;



       A1: ( Chi T) = ( union X) by Th4;

      thus T is first-countable implies ( Chi T) c= omega

      proof

        assume

         A2: for x be Point of T holds ex B be Basis of x st B is countable;

        now

          let a;

          assume a in X;

          then

          consider x be Point of T such that

           A3: a = ( Chi (x,T));

          consider B be Basis of x such that

           A4: B is countable by A2;



           A5: ( card B) c= omega by A4;

          ( Chi (x,T)) c= ( card B) by Def1;

          hence a c= omega by A3, A5;

        end;

        hence thesis by A1, ZFMISC_1: 76;

      end;

      assume

       A6: ( Chi T) c= omega ;

      let x be Point of T;

      consider B be Basis of x such that

       A7: ( Chi (x,T)) = ( card B) by Def1;

      take B;

      ( Chi (x,T)) c= ( Chi T) by Th5;

      hence ( card B) c= omega by A6, A7;

    end;

    begin

    definition

      let T be non empty TopSpace;

      :: TOPGEN_2:def3

      mode Neighborhood_System of T -> ManySortedSet of T means

      : Def3: for x be Element of T holds (it . x) is Basis of x;

      existence

      proof

        set B = the Basis of T;

        deffunc F( Point of T) = { U where U be Subset of T : $1 in U & U in B };

        consider F be ManySortedSet of T such that

         A1: for x be Point of T holds (F . x) = F(x) from PBOOLE:sch 5;

        take F;

        let x be Point of T;

        (F . x) = F(x) by A1;

        hence thesis by Th1;

      end;

    end

    definition

      let T be non empty TopSpace;

      let N be Neighborhood_System of T;

      :: original: Union

      redefine

      func Union N -> Basis of T ;

      coherence

      proof

        for x be Point of T holds (N . x) is Basis of x by Def3;

        hence thesis by Th2;

      end;

      let x be Point of T;

      :: original: .

      redefine

      func N . x -> Basis of x ;

      coherence by Def3;

    end

    theorem :: TOPGEN_2:7

    for T be non empty TopSpace holds for x,y be Point of T holds for B1 be Basis of x, B2 be Basis of y holds for U be set st x in U & U in B2 holds ex V be open Subset of T st V in B1 & V c= U

    proof

      let T be non empty TopSpace;

      let x,y be Point of T;

      let B1 be Basis of x;

      let B2 be Basis of y;

      let U be set;

      assume that

       A1: x in U and

       A2: U in B2;

      U is open Subset of T by A2, YELLOW_8: 12;

      then

      consider V be Subset of T such that

       A3: V in B1 and

       A4: V c= U by A1, YELLOW_8: 13;

      V is open by A3, YELLOW_8: 12;

      hence thesis by A3, A4;

    end;

    theorem :: TOPGEN_2:8

    for T be non empty TopSpace holds for x be Point of T holds for B be Basis of x holds for U1,U2 be set st U1 in B & U2 in B holds ex V be open Subset of T st V in B & V c= (U1 /\ U2)

    proof

      let T be non empty TopSpace;

      let x be Point of T;

      let B be Basis of x;

      let U1,U2 be set;

      assume that

       A1: U1 in B and

       A2: U2 in B;

      reconsider U1, U2 as open Subset of T by A1, A2, YELLOW_8: 12;



       A3: x in U2 by A2, YELLOW_8: 12;

      x in U1 by A1, YELLOW_8: 12;

      then x in (U1 /\ U2) by A3, XBOOLE_0:def 4;

      then

      consider V be Subset of T such that

       A4: V in B and

       A5: V c= (U1 /\ U2) by YELLOW_8: 13;

      V is open by A4, YELLOW_8: 12;

      hence thesis by A4, A5;

    end;

     Lm2:

    now

      let T be non empty TopSpace;

      let A be Subset of T;

      let x be Element of T such that

       A1: x in ( Cl A);

      let B be Basis of x, U be set;

      assume

       A2: U in B;

      then x in U by YELLOW_8: 12;

      then U meets ( Cl A) by A1, XBOOLE_0: 3;

      hence U meets A by A2, TSEP_1: 36, YELLOW_8: 12;

    end;

     Lm3:

    now

      let T be non empty TopSpace;

      let A be Subset of T;

      let x be Element of T;

      given B be Basis of x such that

       A1: for U be set st U in B holds U meets A;

      now

        let U be Subset of T;

        assume that

         A2: U is open and

         A3: x in U;

        ex V be Subset of T st V in B & V c= U by A2, A3, YELLOW_8:def 1;

        hence A meets U by A1, XBOOLE_1: 63;

      end;

      hence x in ( Cl A) by PRE_TOPC:def 7;

    end;

    theorem :: TOPGEN_2:9

    for T be non empty TopSpace holds for A be Subset of T holds for x be Element of T holds x in ( Cl A) iff for B be Basis of x holds for U be set st U in B holds U meets A

    proof

      let T be non empty TopSpace;

      let A be Subset of T;

      let x be Element of T;

      set B = the Basis of x;

      thus x in ( Cl A) implies for B be Basis of x holds for U be set st U in B holds U meets A by Lm2;

      assume for B be Basis of x holds for U be set st U in B holds U meets A;

      then for U be set st U in B holds U meets A;

      hence thesis by Lm3;

    end;

    theorem :: TOPGEN_2:10

    for T be non empty TopSpace holds for A be Subset of T holds for x be Element of T holds x in ( Cl A) iff ex B be Basis of x st for U be set st U in B holds U meets A

    proof

      let T be non empty TopSpace;

      let A be Subset of T;

      let x be Element of T;

      set B = the Basis of x;

      x in ( Cl A) implies for U be set st U in B holds U meets A by Lm2;

      hence x in ( Cl A) implies ex B be Basis of x st for U be set st U in B holds U meets A;

      thus thesis by Lm3;

    end;

    registration

      let T be TopSpace;

      cluster open non empty for Subset-Family of T;

      existence

      proof

        take the topology of T;

        thus thesis;

      end;

    end

    begin

    theorem :: TOPGEN_2:11



     Th11: for T be non empty TopSpace holds for S be open Subset-Family of T holds ex G be open Subset-Family of T st G c= S & ( union G) = ( union S) & ( card G) c= ( weight T)

    proof

      defpred P[ object, object] means ex A,B be set st A = $1 & B = $2 & A c= B;

      let T be non empty TopSpace;

      let S be open Subset-Family of T;

      consider B be Basis of T such that

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

      set B1 = { W where W be Subset of T : W in B & ex U be set st U in S & W c= U };

      B1 c= B

      proof

        let a be object;

        assume a in B1;

        then ex W be Subset of T st a = W & W in B & ex U be set st U in S & W c= U;

        hence thesis;

      end;

      then

       A2: ( card B1) c= ( card B) by CARD_1: 11;

       A3:

      now

        let a be object;

        assume a in B1;

        then ex W be Subset of T st a = W & W in B & ex U be set st U in S & W c= U;

        hence ex b be object st b in S & P[a, b];

      end;

      consider f be Function such that

       A4: ( dom f) = B1 & ( rng f) c= S and

       A5: for a be object st a in B1 holds P[a, (f . a)] from FUNCT_1:sch 6( A3);

      set G = ( rng f);

      reconsider G as open Subset-Family of T by A4, TOPS_2: 11, XBOOLE_1: 1;

      take G;

      thus G c= S & ( union G) c= ( union S) by A4, ZFMISC_1: 77;

      thus ( union S) c= ( union G)

      proof

        let a be object;

        assume a in ( union S);

        then

        consider b such that

         A6: a in b and

         A7: b in S by TARSKI:def 4;

        reconsider b as open Subset of T by A7, TOPS_2:def 1;

        reconsider a as Point of T by A6, A7;

        consider W0 be Subset of T such that

         A8: W0 in B and

         A9: a in W0 and

         A10: W0 c= b by A6, YELLOW_9: 31;



         A11: W0 in B1 by A7, A8, A10;

        then (f . W0) in G by A4, FUNCT_1:def 3;

        then

         A12: (f . W0) c= ( union G) by ZFMISC_1: 74;

         P[W0, (f . W0)] by A5, A11;

        then W0 c= (f . W0);

        then a in (f . W0) by A9;

        hence thesis by A12;

      end;

      ( card G) c= ( card B1) by A4, CARD_1: 12;

      hence thesis by A1, A2;

    end;

    definition

      let T be TopStruct;

      :: TOPGEN_2:def4

      attr T is finite-weight means

      : Def4: ( weight T) is finite;

    end

    notation

      let T be TopStruct;

      antonym T is infinite-weight for T is finite-weight;

    end

    registration

      cluster finite -> finite-weight for TopStruct;

      coherence

      proof

        let T be TopStruct;

        assume

         A1: the carrier of T is finite;

        ex B be Basis of T st ( card B) = ( weight T) by WAYBEL23: 74;

        hence ( weight T) is finite by A1;

      end;

      cluster infinite-weight -> infinite for TopStruct;

      coherence ;

    end

    theorem :: TOPGEN_2:12



     Th12: for X be set holds ( card ( SmallestPartition X)) = ( card X)

    proof

      let X be set;

      set A = ( SmallestPartition X);

      per cases ;

        suppose X = {} ;

        hence thesis;

      end;

        suppose X <> {} ;

        then

        reconsider X as non empty set;

        deffunc F( object) = {$1};



         A1: A = the set of all {x} where x be Element of X by EQREL_1: 37;

        then

         A2: for a be object st a in X holds F(a) in A;

        consider f be Function of X, A such that

         A3: for a be object st a in X holds (f . a) = F(a) from FUNCT_2:sch 2( A2);



         A4: ( rng f) = A

        proof

          thus ( rng f) c= A;

          let a be object;

          assume a in A;

          then

          consider b be Element of X such that

           A5: a = {b} by A1;

          (f . b) = a by A3, A5;

          hence thesis by FUNCT_2: 4;

        end;



         A6: f is one-to-one

        proof

          let a,b be object;

          assume that

           A7: a in ( dom f) and

           A8: b in ( dom f);

          assume (f . a) = (f . b);



          then {a} = (f . b) by A3, A7

          .= {b} by A3, A8;

          hence thesis by ZFMISC_1: 3;

        end;

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

        then (X,A) are_equipotent by A4, A6, WELLORD2:def 4;

        hence thesis by CARD_1: 5;

      end;

    end;

    theorem :: TOPGEN_2:13



     Th13: for T be discrete non empty TopStruct holds ( SmallestPartition the carrier of T) is Basis of T & for B be Basis of T holds ( SmallestPartition the carrier of T) c= B

    proof

      let T be discrete non empty TopStruct;

      set B0 = ( SmallestPartition the carrier of T);



       A1: B0 c= the topology of T

      proof

        let a be object;

        assume a in B0;

        then

        reconsider a as Subset of T;

        a is open by TDLAT_3: 15;

        hence thesis;

      end;



       A2: B0 = the set of all {a} where a be Element of T by EQREL_1: 37;

      now

        let A be Subset of T such that A is open;

        let p be Point of T such that

         A3: p in A;

        reconsider a = {p} as Subset of T;

        take a;

        thus a in B0 by A2;

        thus p in a by TARSKI:def 1;

        thus a c= A by A3, ZFMISC_1: 31;

      end;

      hence

       A4: B0 is Basis of T by A1, YELLOW_9: 32;

      let B be Basis of T;

      let a be object;

      assume

       A5: a in B0;

      then

      consider b be Element of T such that

       A6: a = {b} by A2;

      reconsider a as Subset of T by A5;



       A7: b in a by A6, TARSKI:def 1;

      a is open by A4, A5, YELLOW_8: 10;

      then

      consider U be Subset of T such that

       A8: U in B and

       A9: b in U and

       A10: U c= a by A7, YELLOW_9: 31;

      a c= U by A6, A9, ZFMISC_1: 31;

      hence thesis by A8, A10, XBOOLE_0:def 10;

    end;

    theorem :: TOPGEN_2:14



     Th14: for T be discrete non empty TopStruct holds ( weight T) = ( card the carrier of T)

    proof

      let T be discrete non empty TopStruct;

      set M = the set of all ( card C) where C be Basis of T;

      reconsider B0 = ( SmallestPartition the carrier of T) as Basis of T by Th13;



       A1: ( card B0) in M;



       A2: ( card B0) = ( card the carrier of T) by Th12;

      ( weight T) = ( meet M) by WAYBEL23:def 5;

      hence ( weight T) c= ( card the carrier of T) by A2, A1, SETFAM_1: 3;

      ex B be Basis of T st ( card B) = ( weight T) by WAYBEL23: 74;

      hence ( card the carrier of T) c= ( weight T) by A2, Th13, CARD_1: 11;

    end;

    registration

      cluster infinite-weight for TopSpace;

      existence

      proof

        set A = the infinite set;

        reconsider O = ( bool A) as Subset-Family of A;

        reconsider T = TopStruct (# A, O #) as discrete non empty TopStruct by TDLAT_3:def 1;

        take T;

        ( weight T) = ( card the carrier of T) by Th14;

        hence ( weight T) is infinite;

      end;

    end



     Lm4: for T be infinite-weight TopSpace holds for B be Basis of T holds ex B1 be Basis of T st B1 c= B & ( card B1) = ( weight T)

    proof

      let T be infinite-weight TopSpace;

      let B be Basis of T;

      consider B0 be Basis of T such that

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

      defpred P[ object, object] means ex A be set st A = $2 & ( union A) = $1 & ( card A) c= ( weight T);

       A2:

      now

        let a be object;

        reconsider aa = a as set by TARSKI: 1;

        set Sa = { U where U be Subset of T : U in B & U c= aa };



         A3: Sa c= B

        proof

          let b be object;

          assume b in Sa;

          then ex U be Subset of T st b = U & U in B & U c= aa;

          hence thesis;

        end;

        assume a in B0;

        then

        reconsider W = a as open Subset of T by YELLOW_8: 10;



         A4: ( union Sa) = W by YELLOW_8: 9;

        reconsider Sa as open Subset-Family of T by A3, TOPS_2: 11, XBOOLE_1: 1;

        consider G be open Subset-Family of T such that

         A5: G c= Sa and

         A6: ( union G) = ( union Sa) and

         A7: ( card G) c= ( weight T) by Th11;

        reconsider b = G as object;

        take b;

        G c= B by A3, A5;

        hence b in ( bool B);

        thus P[a, b] by A4, A6, A7;

      end;

      consider f be Function such that

       A8: ( dom f) = B0 & ( rng f) c= ( bool B) and

       A9: for a be object st a in B0 holds P[a, (f . a)] from FUNCT_1:sch 6( A2);



       A10: ( Union f) c= ( union ( bool B)) by A8, ZFMISC_1: 77;

      then

       A11: ( Union f) c= B by ZFMISC_1: 81;

      then

      reconsider B1 = ( Union f) as Subset-Family of T by XBOOLE_1: 1;

      now

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

        hence B1 c= the topology of T by A11;

        let A be Subset of T such that

         A12: A is open;

        let p be Point of T;

        assume p in A;

        then

        consider U be Subset of T such that

         A13: U in B0 and

         A14: p in U and

         A15: U c= A by A12, YELLOW_9: 31;



         A16: P[U, (f . U)] by A9, A13;

        then

        consider a such that

         A17: p in a and

         A18: a in (f . U) by A14, TARSKI:def 4;



         A19: a c= U by A16, A18, ZFMISC_1: 74;

        a in B1 by A8, A13, A18, CARD_5: 2;

        hence ex a be Subset of T st a in B1 & p in a & a c= A by A15, A17, A19, XBOOLE_1: 1;

      end;

      then

      reconsider B1 as Basis of T by YELLOW_9: 32;

      now

        thus ( card ( rng f)) c= ( weight T) by A1, A8, CARD_1: 12;

        let a;

        assume a in ( rng f);

        then

        consider b be object such that

         A20: b in ( dom f) & a = (f . b) by FUNCT_1:def 3;

         P[b, (f . b)] by A8, A9, A20;

        hence ( card a) c= ( weight T) by A20;

      end;

      then

       A21: ( card B1) c= (( weight T) *` ( weight T)) by CARD_2: 87;

      take B1;

      thus B1 c= B by A10, ZFMISC_1: 81;

      ( weight T) is infinite by Def4;

      hence ( card B1) c= ( weight T) by A21, CARD_4: 15;

      thus thesis by WAYBEL23: 73;

    end;

    theorem :: TOPGEN_2:15



     Th15: for T be finite-weight non empty TopSpace holds ex B0 be Basis of T st ex f be Function of the carrier of T, the topology of T st B0 = ( rng f) & for x be Point of T holds x in (f . x) & for U be open Subset of T st x in U holds (f . x) c= U

    proof

      let T be finite-weight non empty TopSpace;

      consider B be Basis of T such that

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

      deffunc F( object) = ( meet { U where U be Subset of T : $1 in U & U in B });



       A2: B is finite by A1, Def4;

       A3:

      now

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

        then ( FinMeetCl B) c= ( FinMeetCl the topology of T) by CANTOR_1: 14;

        then

         A4: ( FinMeetCl B) c= the topology of T by CANTOR_1: 5;

        let a be object;

        assume a in the carrier of T;

        then

        reconsider x = a as Point of T;

        set S = { U where U be Subset of T : x in U & U in B };

        consider U be Subset of T such that

         A5: U in B and

         A6: x in U and U c= ( [#] T) by YELLOW_9: 31;



         A7: S c= B

        proof

          let a be object;

          assume a in S;

          then ex U be Subset of T st a = U & x in U & U in B;

          hence thesis;

        end;

        then

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

        ( Intersect S) in ( FinMeetCl B) by A2, A7, CANTOR_1:def 3;

        then

         A8: ( Intersect S) in the topology of T by A4;

        U in S by A5, A6;

        hence F(a) in the topology of T by A8, SETFAM_1:def 9;

      end;

      consider f be Function of the carrier of T, the topology of T such that

       A9: for a be object st a in the carrier of T holds (f . a) = F(a) from FUNCT_2:sch 2( A3);

      set B0 = ( rng f);

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

       A10:

      now

        let a;

        assume a in the carrier of T;

        then

        reconsider x = a as Point of T;

        set S = { U where U be Subset of T : x in U & U in B };

        consider U be Subset of T such that

         A11: U in B and

         A12: x in U and U c= ( [#] T) by YELLOW_9: 31;

         A13:

        now

          let b;

          assume b in S;

          then ex U be Subset of T st b = U & a in U & U in B;

          hence a in b;

        end;



         A14: (f . a) = ( meet S) by A9;

        U in S by A11, A12;

        hence a in (f . a) by A14, A13, SETFAM_1:def 1;

      end;

       A15:

      now

        let x be Point of T, V be Subset of T;

        set S = { U where U be Subset of T : x in U & U in B };

        assume that

         A16: x in V and

         A17: V is open;

        consider U be Subset of T such that

         A18: U in B and

         A19: x in U and

         A20: U c= V by A16, A17, YELLOW_9: 31;



         A21: (f . x) = ( meet S) by A9;

        U in S by A18, A19;

        then (f . x) c= U by A21, SETFAM_1: 3;

        hence (f . x) c= V by A20;

      end;

      now

        let A be Subset of T;

        assume

         A22: A is open;

        let p be Point of T;

        assume

         A23: p in A;

        (f . p) in the topology of T;

        then

        reconsider a = (f . p) as Subset of T;

        take a;

        thus a in B0 by FUNCT_2: 4;

        thus p in a by A10;

        thus a c= A by A15, A22, A23;

      end;

      then

      reconsider B0 as Basis of T by YELLOW_9: 32;

      take B0, f;

      thus B0 = ( rng f);

      let x be Point of T;

      thus thesis by A10, A15;

    end;

    theorem :: TOPGEN_2:16



     Th16: for T be TopSpace holds for B0,B be Basis of T holds for f be Function of the carrier of T, the topology of T st B0 = ( rng f) & for x be Point of T holds x in (f . x) & for U be open Subset of T st x in U holds (f . x) c= U holds B0 c= B

    proof

      let T be TopSpace;

      let B0,B be Basis of T;

      let f be Function of the carrier of T, the topology of T;

      assume

       A1: B0 = ( rng f);

      assume

       A2: for x be Point of T holds x in (f . x) & for U be open Subset of T st x in U holds (f . x) c= U;

      let a be object;

      assume

       A3: a in B0;

      then

      reconsider V = a as Subset of T;

      consider b be object such that

       A4: b in ( dom f) and

       A5: a = (f . b) by A1, A3, FUNCT_1:def 3;



       A6: V is open by A3, YELLOW_8: 10;

      reconsider b as Element of T by A4;

      b in V by A2, A5;

      then

      consider U be Subset of T such that

       A7: U in B and

       A8: b in U and

       A9: U c= V by A6, YELLOW_9: 31;

      U is open by A7, YELLOW_8: 10;

      then (f . b) c= U by A2, A8;

      hence thesis by A7, A9, XBOOLE_0:def 10, A5;

    end;

    theorem :: TOPGEN_2:17



     Th17: for T be TopSpace holds for B0 be Basis of T holds for f be Function of the carrier of T, the topology of T st B0 = ( rng f) & for x be Point of T holds x in (f . x) & for U be open Subset of T st x in U holds (f . x) c= U holds ( weight T) = ( card B0)

    proof

      let T be TopSpace;

      let B0 be Basis of T;

      let f be Function of the carrier of T, the topology of T such that

       A1: B0 = ( rng f) and

       A2: for x be Point of T holds x in (f . x) & for U be open Subset of T st x in U holds (f . x) c= U;

      set M = the set of all ( card C) where C be Basis of T;



       A3: ( card B0) in M;

      ( weight T) = ( meet M) by WAYBEL23:def 5;

      hence ( weight T) c= ( card B0) by A3, SETFAM_1: 3;

      ex B be Basis of T st ( card B) = ( weight T) by WAYBEL23: 74;

      hence thesis by A1, A2, Th16, CARD_1: 11;

    end;



     Lm5: for T be finite-weight non empty TopSpace holds for B be Basis of T holds ex B1 be Basis of T st B1 c= B & ( card B1) = ( weight T)

    proof

      let T be finite-weight non empty TopSpace;

      let B be Basis of T;

      consider B0 be Basis of T, f be Function of the carrier of T, the topology of T such that

       A1: B0 = ( rng f) and

       A2: for x be Point of T holds x in (f . x) & for U be open Subset of T st x in U holds (f . x) c= U by Th15;

      take B0;

      thus B0 c= B by A1, A2, Th16;

      thus ( card B0) c= ( weight T) by A1, A2, Th17;

      thus thesis by WAYBEL23: 73;

    end;

    theorem :: TOPGEN_2:18

    for T be non empty TopSpace holds for B be Basis of T holds ex B1 be Basis of T st B1 c= B & ( card B1) = ( weight T)

    proof

      let T be non empty TopSpace, B be Basis of T;

      T is finite-weight or T is infinite-weight;

      hence thesis by Lm4, Lm5;

    end;

    begin

    definition

      let X,x0 be set;

      :: TOPGEN_2:def5

      func DiscrWithInfin (X,x0) -> strict TopStruct means

      : Def5: the carrier of it = X & the topology of it = ({ U where U be Subset of X : not x0 in U } \/ { (F ` ) where F be Subset of X : F is finite });

      uniqueness ;

      existence

      proof

        set O1 = { U where U be Subset of X : not x0 in U }, O2 = { (F ` ) where F be Subset of X : F is finite }, O = (O1 \/ O2);

        O c= ( bool X)

        proof

          let a be object;

          assume a in O;

          then a in O1 or a in O2 by XBOOLE_0:def 3;

          then (ex U be Subset of X st a = U & not x0 in U) or ex F be Subset of X st a = (F ` ) & F is finite;

          hence thesis;

        end;

        then

        reconsider O as Subset-Family of X;

        take TopStruct (# X, O #);

        thus thesis;

      end;

    end

    registration

      let X,x0 be set;

      cluster ( DiscrWithInfin (X,x0)) -> TopSpace-like;

      coherence

      proof

        set O1 = { U where U be Subset of X : not x0 in U }, O2 = { (F ` ) where F be Subset of X : F is finite }, O = (O1 \/ O2);

        set T = ( DiscrWithInfin (X,x0));



         A1: the carrier of T = X by Def5;



         A2: the topology of T = O by Def5;

        (( {} X) ` ) = X;

        then X in O2;

        hence the carrier of T in the topology of T by A1, A2, XBOOLE_0:def 3;

        hereby

          let a be Subset-Family of T such that

           A3: a c= the topology of T;

          per cases ;

            suppose not a c= O1;

            then

            consider b be object such that

             A4: b in a and

             A5: not b in O1;

            reconsider bb = b as set by TARSKI: 1;

            b in O2 by A2, A3, A4, A5, XBOOLE_0:def 3;

            then

             A6: ex F be Subset of X st b = (F ` ) & F is finite;



             A7: ((( union a) ` ) ` ) = ( union a);

            bb c= ( union a) by A4, ZFMISC_1: 74;

            then (( union a) ` ) is finite by A1, A6, FINSET_1: 1, SUBSET_1: 17;

            then ( union a) in O2 by A1, A7;

            hence ( union a) in the topology of T by A2, XBOOLE_0:def 3;

          end;

            suppose

             A8: a c= O1;

            now

              assume x0 in ( union a);

              then

              consider b such that

               A9: x0 in b and

               A10: b in a by TARSKI:def 4;

              b in O1 by A8, A10;

              then ex U be Subset of X st b = U & not x0 in U;

              hence contradiction by A9;

            end;

            then ( union a) in O1 by A1;

            hence ( union a) in the topology of T by A2, XBOOLE_0:def 3;

          end;

        end;

        let a,b be Subset of T;

        assume that

         A11: a in the topology of T and

         A12: b in the topology of T;

        per cases by A2, A11, A12, XBOOLE_0:def 3;

          suppose

           A13: a in O2 & b in O2;

          then

          consider F2 be Subset of X such that

           A14: b = (F2 ` ) and

           A15: F2 is finite;

          consider F1 be Subset of X such that

           A16: a = (F1 ` ) and

           A17: F1 is finite by A13;

          (a /\ b) = ((F1 \/ F2) ` ) by A16, A14, XBOOLE_1: 53;

          then (a /\ b) in O2 by A17, A15;

          hence thesis by A2, XBOOLE_0:def 3;

        end;

          suppose a in O1 or b in O1;

          then (ex U be Subset of X st a = U & not x0 in U) or ex U be Subset of X st b = U & not x0 in U;

          then not x0 in (a /\ b) by XBOOLE_0:def 4;

          then (a /\ b) in O1 by A1;

          hence thesis by A2, XBOOLE_0:def 3;

        end;

      end;

    end

    registration

      let X be non empty set, x0 be set;

      cluster ( DiscrWithInfin (X,x0)) -> non empty;

      coherence by Def5;

    end

    theorem :: TOPGEN_2:19



     Th19: for X,x0 be set, A be Subset of ( DiscrWithInfin (X,x0)) holds A is open iff not x0 in A or (A ` ) is finite

    proof

      let X,x0 be set;

      set T = ( DiscrWithInfin (X,x0));

      set O1 = { U where U be Subset of X : not x0 in U };

      set O2 = { (F ` ) where F be Subset of X : F is finite };

      let A be Subset of T;



       A1: the topology of T = (O1 \/ O2) by Def5;



       A2: the carrier of T = X by Def5;

      thus A is open implies not x0 in A or (A ` ) is finite

      proof

        assume A in the topology of T;

        then A in O1 or A in O2 by A1, XBOOLE_0:def 3;

        then (ex U be Subset of X st A = U & not x0 in U) or ex F be Subset of X st A = (F ` ) & F is finite;

        hence thesis by A2;

      end;

      assume not x0 in A or (A ` ) is finite;

      then A in O1 or ((A ` ) ` ) in O2 by A2;

      hence A in the topology of T by A1, XBOOLE_0:def 3;

    end;

    theorem :: TOPGEN_2:20



     Th20: for X,x0 be set, A be Subset of ( DiscrWithInfin (X,x0)) holds A is closed iff (x0 in X implies x0 in A) or A is finite

    proof

      let X,x0 be set;

      set T = ( DiscrWithInfin (X,x0));

      let A be Subset of ( DiscrWithInfin (X,x0));



       A1: A is closed iff not x0 in (A ` ) or ((A ` ) ` ) is finite by Th19;

      the carrier of T = X by Def5;

      hence thesis by A1, XBOOLE_0:def 5;

    end;

    theorem :: TOPGEN_2:21

    for X,x0,x be set st x in X holds {x} is closed Subset of ( DiscrWithInfin (X,x0))

    proof

      let X,x0,x be set;

      set T = ( DiscrWithInfin (X,x0));

      the carrier of T = X by Def5;

      hence thesis by Th20, ZFMISC_1: 31;

    end;

    theorem :: TOPGEN_2:22



     Th22: for X,x0,x be set st x in X & x <> x0 holds {x} is open Subset of ( DiscrWithInfin (X,x0))

    proof

      let X,x0,x be set;

      set T = ( DiscrWithInfin (X,x0));

      assume that

       A1: x in X and

       A2: x <> x0;



       A3: the carrier of T = X by Def5;

       not x0 in {x} by A2, TARSKI:def 1;

      hence thesis by A3, A1, Th19, ZFMISC_1: 31;

    end;

    theorem :: TOPGEN_2:23

    for X,x0 be set st X is infinite holds for U be Subset of ( DiscrWithInfin (X,x0)) st U = {x0} holds not U is open

    proof

      let X,x0 be set;

      set T = ( DiscrWithInfin (X,x0));

      assume

       A1: X is infinite;

      let U be Subset of ( DiscrWithInfin (X,x0));

      assume

       A2: U = {x0};

      the carrier of T = X by Def5;

      then X = ((U ` ) \/ {x0}) by A2, XBOOLE_1: 45;

      then

       A3: (U ` ) is infinite by A1;

      x0 in U by A2, TARSKI:def 1;

      hence thesis by A3, Th19;

    end;

    theorem :: TOPGEN_2:24



     Th24: for X,x0 be set holds for A be Subset of ( DiscrWithInfin (X,x0)) st A is finite holds ( Cl A) = A

    proof

      let X,x0 be set;

      let A be Subset of ( DiscrWithInfin (X,x0));

      assume A is finite;

      then A is closed by Th20;

      hence thesis by PRE_TOPC: 22;

    end;

    theorem :: TOPGEN_2:25



     Th25: for T be non empty TopSpace holds for A be Subset of T st not A is closed holds for a be Point of T st (A \/ {a}) is closed holds ( Cl A) = (A \/ {a})

    proof

      let T be non empty TopSpace;

      let A be Subset of T such that

       A1: not A is closed;



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

      let a be Point of T;

      assume (A \/ {a}) is closed;

      then

       A3: ( Cl (A \/ {a})) = (A \/ {a}) by PRE_TOPC: 22;

      ( Cl A) c= ( Cl (A \/ {a})) by PRE_TOPC: 19, XBOOLE_1: 7;

      hence thesis by A1, A2, A3, ZFMISC_1: 138;

    end;

    theorem :: TOPGEN_2:26



     Th26: for X,x0 be set st x0 in X holds for A be Subset of ( DiscrWithInfin (X,x0)) st A is infinite holds ( Cl A) = (A \/ {x0})

    proof

      let X,x0 be set such that

       A1: x0 in X;

      set T = ( DiscrWithInfin (X,x0));

      reconsider T as non empty TopSpace by A1;

      reconsider x = x0 as Point of T by A1, Def5;

      let A be Subset of ( DiscrWithInfin (X,x0));

      reconsider B = {x} as Subset of T;

      reconsider A9 = A as Subset of T;

      x0 in {x0} by TARSKI:def 1;

      then x0 in (A9 \/ B) by XBOOLE_0:def 3;

      then (A9 \/ B) is closed by Th20;

      then

       A2: ( Cl (A9 \/ B)) = (A9 \/ B) by PRE_TOPC: 22;

      assume A is infinite;

      then not A9 is closed or x0 in A by A1, Th20;

      hence thesis by A2, Th25, ZFMISC_1: 40;

    end;

    theorem :: TOPGEN_2:27

    for X,x0 be set holds for A be Subset of ( DiscrWithInfin (X,x0)) st (A ` ) is finite holds ( Int A) = A

    proof

      let X,x0 be set;

      let A be Subset of ( DiscrWithInfin (X,x0));

      assume (A ` ) is finite;

      then ( Cl (A ` )) = (A ` ) by Th24;



      hence ( Int A) = ((A ` ) ` ) by TOPS_1:def 1

      .= A;

    end;

    theorem :: TOPGEN_2:28

    for X,x0 be set st x0 in X holds for A be Subset of ( DiscrWithInfin (X,x0)) st (A ` ) is infinite holds ( Int A) = (A \ {x0})

    proof

      let X,x0 be set such that

       A1: x0 in X;

      set T = ( DiscrWithInfin (X,x0));

      reconsider T as non empty TopSpace by A1;

      reconsider x = x0 as Point of T by A1, Def5;

      let A be Subset of ( DiscrWithInfin (X,x0));

      reconsider A9 = A as Subset of T;

      assume (A ` ) is infinite;

      then ( Cl (A ` )) = ((A9 ` ) \/ {x}) by A1, Th26;



      hence ( Int A) = (((A9 ` ) \/ {x}) ` ) by TOPS_1:def 1

      .= (((A9 \ {x}) ` ) ` ) by SUBSET_1: 14

      .= (A \ {x0});

    end;

    theorem :: TOPGEN_2:29



     Th29: for X,x0 be set holds ex B0 be Basis of ( DiscrWithInfin (X,x0)) st B0 = ((( SmallestPartition X) \ { {x0}}) \/ { (F ` ) where F be Subset of X : F is finite })

    proof

      let X,x0 be set;

      set T = ( DiscrWithInfin (X,x0));

      set B1 = (( SmallestPartition X) \ { {x0}});

      set B2 = { (F ` ) where F be Subset of X : F is finite };



       A1: B1 c= the topology of T

      proof

        let a be object;

        reconsider aa = a as set by TARSKI: 1;

        assume

         A2: a in B1;

        then

         A3: a in ( SmallestPartition X) by ZFMISC_1: 56;

        then

        reconsider X as non empty set;

        ( SmallestPartition X) = the set of all {x} where x be Element of X by EQREL_1: 37;

        then

         A4: ex x be Element of X st a = {x} by A3;

        a <> {x0} by A2, ZFMISC_1: 56;

        then not x0 in aa by A4, TARSKI:def 1;

        then a is open Subset of T by A2, Def5, Th19;

        hence thesis by PRE_TOPC:def 2;

      end;



       A5: the carrier of T = X by Def5;

      B2 c= ( bool the carrier of T)

      proof

        let a be object;

        assume a in B2;

        then ex F be Subset of X st a = (F ` ) & F is finite;

        hence thesis by A5;

      end;

      then

      reconsider B0 = (B1 \/ B2) as Subset-Family of T by A5, XBOOLE_1: 8;

       A6:

      now

        let A be Subset of T;

        assume A is open;

        then

         A7: not x0 in A or (A ` ) is finite by Th19;

        let p be Point of T such that

         A8: p in A;

        reconsider X9 = X as non empty set by A8, Def5;

        reconsider p9 = p as Element of X9 by Def5;

        ( SmallestPartition X) = the set of all {x} where x be Element of X9 by EQREL_1: 37;

        then

         A9: {p9} in ( SmallestPartition X);

         {p} <> {x0} or ((A ` ) ` ) in B2 by A5, A8, A7, ZFMISC_1: 3;

        then not {p} in { {x0}} or A in B2 by TARSKI:def 1;

        then {p} in B1 or A in B2 by A9, XBOOLE_0:def 5;

        then {p} in B0 & p in {p} & {p} c= A or A in B0 & A c= A by A8, XBOOLE_0:def 3, ZFMISC_1: 31;

        hence ex a be Subset of T st a in B0 & p in a & a c= A by A8;

      end;

      B2 c= the topology of T

      proof

        let a be object;

        assume a in B2;

        then

        consider F be Subset of X such that

         A10: a = (F ` ) and

         A11: F is finite;

        ((F ` ) ` ) is finite by A11;

        then a is open Subset of T by A5, A10, Th19;

        hence thesis by PRE_TOPC:def 2;

      end;

      then

      reconsider B0 as Basis of ( DiscrWithInfin (X,x0)) by A1, A6, XBOOLE_1: 8, YELLOW_9: 32;

      take B0;

      thus thesis;

    end;

    theorem :: TOPGEN_2:30

    for X be infinite set holds ( card ( Fin X)) = ( card X)

    proof

      deffunc f( set) = ( proj2 $1);

      let X be infinite set;

      set FX = ( Fin X);

      consider f be Function such that

       A1: ( dom f) = (X * ) & for a st a in (X * ) holds (f . a) = f(a) from FUNCT_1:sch 5;

      FX c= ( rng f)

      proof

        let a be object;

        reconsider aa = a as set by TARSKI: 1;

        assume

         A2: a in FX;

        then aa is finite by FINSUB_1:def 5;

        then

        consider p be FinSequence such that

         A3: a = ( rng p) by FINSEQ_1: 52;

        aa c= X by A2, FINSUB_1:def 5;

        then p is FinSequence of X by A3, FINSEQ_1:def 4;

        then

         A4: p in (X * ) by FINSEQ_1:def 11;

        then (f . p) in ( rng f) by A1, FUNCT_1:def 3;

        hence thesis by A1, A3, A4;

      end;

      then ( card FX) c= ( card (X * )) by A1, CARD_1: 12;

      hence ( card FX) c= ( card X) by CARD_4: 24;

      set SX = ( SmallestPartition X);

      SX c= FX

      proof

        let a be object;

        assume a in SX;

        then a in the set of all {x} where x be Element of X by EQREL_1: 37;

        then ex x be Element of X st a = {x};

        hence thesis by FINSUB_1:def 5;

      end;

      then ( card SX) c= ( card FX) by CARD_1: 11;

      hence thesis by Th12;

    end;

    theorem :: TOPGEN_2:31



     Th31: for X be infinite set holds ( card { (F ` ) where F be Subset of X : F is finite }) = ( card X)

    proof

      let X be infinite set;

      set FX = { (F ` ) where F be Subset of X : F is finite };

      deffunc f( set) = (X \ ( proj2 $1));

      consider f be Function such that

       A1: ( dom f) = (X * ) & for a st a in (X * ) holds (f . a) = f(a) from FUNCT_1:sch 5;

      FX c= ( rng f)

      proof

        let a be object;

        assume a in FX;

        then

        consider F be Subset of X such that

         A2: a = (F ` ) and

         A3: F is finite;

        consider p be FinSequence such that

         A4: F = ( rng p) by A3, FINSEQ_1: 52;

        p is FinSequence of X by A4, FINSEQ_1:def 4;

        then

         A5: p in (X * ) by FINSEQ_1:def 11;

        then (f . p) in ( rng f) by A1, FUNCT_1:def 3;

        hence thesis by A1, A2, A4, A5;

      end;

      then ( card FX) c= ( card (X * )) by A1, CARD_1: 12;

      hence ( card FX) c= ( card X) by CARD_4: 24;

      deffunc f( set) = (X \ {$1});

      consider f be Function such that

       A6: ( dom f) = X & for a st a in X holds (f . a) = f(a) from FUNCT_1:sch 5;



       A7: ( rng f) c= FX

      proof

        let a be object;

        assume a in ( rng f);

        then

        consider b be object such that

         A8: b in ( dom f) and

         A9: a = (f . b) by FUNCT_1:def 3;

        reconsider b as Element of X by A6, A8;

        ( {b} ` ) in FX;

        hence thesis by A6, A9;

      end;

      f is one-to-one

      proof

        let a,b be object;

        assume that

         A10: a in ( dom f) and

         A11: b in ( dom f) and

         A12: (f . a) = (f . b);

        reconsider a, b as Element of X by A6, A10, A11;

        ( {a} ` ) = (f . b) by A6, A12

        .= ( {b} ` ) by A6;

        then {a} = {b} by SUBSET_1: 42;

        hence thesis by ZFMISC_1: 3;

      end;

      hence thesis by A6, A7, CARD_1: 10;

    end;

    theorem :: TOPGEN_2:32



     Th32: for X be infinite set, x0 be set holds for B0 be Basis of ( DiscrWithInfin (X,x0)) st B0 = ((( SmallestPartition X) \ { {x0}}) \/ { (F ` ) where F be Subset of X : F is finite }) holds ( card B0) = ( card X)

    proof

      let X be infinite set;

      let x0 be set;

      set T = ( DiscrWithInfin (X,x0));

      let B0 be Basis of T;

      set SX = ( SmallestPartition X), FX = { (F ` ) where F be Subset of X : F is finite };

      assume

       A1: B0 = ((SX \ { {x0}}) \/ FX);



       A2: ( card SX) = ( card X) by Th12;



       A3: ( card { {x0}}) = 1 by CARD_1: 30;



       A4: 1 in ( card X) by CARD_3: 86;

      then (( card X) +` 1) = ( card X) by CARD_2: 76;

      then

       A5: ( card (SX \ { {x0}})) = ( card X) by A3, A2, A4, CARD_2: 98;

      ( card FX) = ( card X) by Th31;

      then ( card B0) c= (( card X) +` ( card X)) by A1, A5, CARD_2: 34;

      hence ( card B0) c= ( card X) by CARD_2: 75;

      thus thesis by A1, A5, CARD_1: 11, XBOOLE_1: 7;

    end;

    theorem :: TOPGEN_2:33



     Th33: for X be infinite set, x0 be set holds for B be Basis of ( DiscrWithInfin (X,x0)) holds ( card X) c= ( card B)

    proof

      let X be infinite set;

      let x0 be set;

      set T = ( DiscrWithInfin (X,x0));

      set SX = ( SmallestPartition X);



       A1: ( card { {x0}}) = 1 by CARD_1: 30;



       A2: ( card SX) = ( card X) by Th12;

      let B be Basis of T;



       A3: the carrier of T = X by Def5;



       A4: SX = the set of all {x} where x be Element of X by EQREL_1: 37;



       A5: (SX \ { {x0}}) c= B

      proof

        let a be object;

        reconsider aa = a as set by TARSKI: 1;

        assume

         A6: a in (SX \ { {x0}});

        then not a in { {x0}} by XBOOLE_0:def 5;

        then

         A7: a <> {x0} by TARSKI:def 1;

        a in SX by A6, XBOOLE_0:def 5;

        then ex x be Element of X st a = {x} by A4;

        then

        consider x be Element of T such that

         A8: a = {x} and

         A9: x <> x0 by A3, A7;



         A10: x in aa by A8, TARSKI:def 1;

        a is open Subset of T by A3, A8, A9, Th22;

        then

        consider U be Subset of T such that

         A11: U in B and

         A12: x in U and

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

        aa c= U by A8, A12, ZFMISC_1: 31;

        hence thesis by A11, A13, XBOOLE_0:def 10;

      end;



       A14: 1 in ( card X) by CARD_3: 86;

      then (( card X) +` 1) = ( card X) by CARD_2: 76;

      then ( card (SX \ { {x0}})) = ( card X) by A1, A2, A14, CARD_2: 98;

      hence thesis by A5, CARD_1: 11;

    end;

    theorem :: TOPGEN_2:34

    for X be infinite set, x0 be set holds ( weight ( DiscrWithInfin (X,x0))) = ( card X)

    proof

      let X be infinite set;

      let x0 be set;

      set T = ( DiscrWithInfin (X,x0));

      consider B0 be Basis of T such that

       A1: B0 = ((( SmallestPartition X) \ { {x0}}) \/ { (F ` ) where F be Subset of X : F is finite }) by Th29;

      ( card B0) = ( card X) by A1, Th32;

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

      ex B be Basis of T st ( card B) = ( weight T) by WAYBEL23: 74;

      hence thesis by Th33;

    end;

    theorem :: TOPGEN_2:35

    for X be non empty set, x0 be set holds ex B0 be prebasis of ( DiscrWithInfin (X,x0)) st B0 = ((( SmallestPartition X) \ { {x0}}) \/ the set of all ( {x} ` ) where x be Element of X)

    proof

      let X be non empty set;

      let x0 be set;

      set T = ( DiscrWithInfin (X,x0));

      set SX = ( SmallestPartition X), FX = { (F ` ) where F be Subset of X : F is finite }, AX = the set of all ( {x} ` ) where x be Element of X;

      reconsider SX as Subset-Family of T by Def5;

      AX c= ( bool X)

      proof

        let a be object;

        assume a in AX;

        then ex x be Element of X st a = ( {x} ` );

        hence thesis;

      end;

      then

      reconsider AX as Subset-Family of T by Def5;

      reconsider pB = ((SX \ { {x0}}) \/ AX) as Subset-Family of T;

      consider B0 be Basis of T such that

       A1: B0 = ((( SmallestPartition X) \ { {x0}}) \/ FX) by Th29;



       A2: the carrier of T = X by Def5;



       A3: FX c= ( FinMeetCl pB)

      proof

        let a be object;

        assume a in FX;

        then

        consider F be Subset of T such that

         A4: a = (F ` ) and

         A5: F is finite by A2;

        set SF = ( SmallestPartition F);

        ( bool F) c= ( bool X) by A2, ZFMISC_1: 67;

        then

        reconsider SF as Subset-Family of T by A2, XBOOLE_1: 1;

        per cases ;

          suppose F = {} ;

          hence thesis by A4, CANTOR_1: 8;

        end;

          suppose F <> {} ;

          then

          reconsider F as non empty Subset of T;

          SF is a_partition of F;

          then

          reconsider SF as non empty Subset-Family of T;



           A6: ( COMPLEMENT SF) c= pB

          proof

            let a be object;

            assume

             A7: a in ( COMPLEMENT SF);

            then

            reconsider a as Subset of T;

            (a ` ) in SF by A7, SETFAM_1:def 7;

            then (a ` ) in the set of all {b} where b be Element of F by EQREL_1: 37;

            then

            consider b be Element of F such that

             A8: (a ` ) = {b};

            reconsider b as Element of X by Def5;

            ( {b} ` ) in AX;

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

          end;

          F = ( union SF) by EQREL_1:def 4;

          then

           A9: a = ( meet ( COMPLEMENT SF)) by A4, TOPS_2: 6;

          ( COMPLEMENT SF) is finite by A5, TOPS_2: 8;

          then ( Intersect ( COMPLEMENT SF)) in ( FinMeetCl pB) by A6, CANTOR_1:def 3;

          hence thesis by A9, SETFAM_1:def 9;

        end;

      end;



       A10: pB c= ( FinMeetCl pB) by CANTOR_1: 4;



       A11: B0 c= ( FinMeetCl pB)

      proof

        let a be object;

        assume a in B0;

        then a in (SX \ { {x0}}) or a in FX by A1, XBOOLE_0:def 3;

        then a in pB or a in FX by XBOOLE_0:def 3;

        hence thesis by A10, A3;

      end;



       A12: B0 c= the topology of T by TOPS_2: 64;

      AX c= FX

      proof

        let a be object;

        assume a in AX;

        then ex x be Element of X st a = ( {x} ` );

        hence thesis;

      end;

      then pB c= B0 by A1, XBOOLE_1: 9;

      then pB c= the topology of T by A12;

      then ( FinMeetCl pB) c= ( FinMeetCl the topology of T) by CANTOR_1: 14;

      then ( FinMeetCl pB) c= the topology of T by CANTOR_1: 5;

      then ( FinMeetCl pB) is Basis of T by A11, WAYBEL19: 22;

      then pB is prebasis of T by YELLOW_9: 23;

      hence thesis;

    end;

    begin

    theorem :: TOPGEN_2:36

    for T be TopSpace, F be Subset-Family of T holds for I be non empty Subset-Family of F st for G be set st G in I holds (F \ G) is finite holds ( Cl ( union F)) = (( union ( clf F)) \/ ( meet { ( Cl ( union G)) where G be Subset-Family of T : G in I }))

    proof

      let T be TopSpace;

      let F be Subset-Family of T;

      let I be non empty Subset-Family of F;

      set G0 = the Element of I;

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

      set Z = { ( Cl ( union G)) where G be Subset-Family of T : G in I };



       A1: ( Cl ( union G0)) in Z;

      then

      reconsider Z9 = Z as non empty set;

      assume

       A2: for G be set st G in I holds (F \ G) is finite;

      thus ( Cl ( union F)) c= (( union ( clf F)) \/ ( meet Z))

      proof

        let a be object;

        assume that

         A3: a in ( Cl ( union F)) and

         A4: not a in (( union ( clf F)) \/ ( meet Z));

        reconsider a as Point of T by A3;

         not a in ( meet Z9) by A4, XBOOLE_0:def 3;

        then

        consider b such that

         A5: b in Z and

         A6: not a in b by SETFAM_1:def 1;

        consider G be Subset-Family of T such that

         A7: b = ( Cl ( union G)) and

         A8: G in I by A5;



         A9: T is non empty by A3;

        then ( clf (F \ G)) c= ( clf F) by PCOMPS_1: 14, XBOOLE_1: 36;

        then

         A10: ( union ( clf (F \ G))) c= ( union ( clf F)) by ZFMISC_1: 77;

        F = (G \/ (F \ G)) by A8, XBOOLE_1: 45;

        then ( union F) = (( union G) \/ ( union (F \ G))) by ZFMISC_1: 78;

        then ( Cl ( union F)) = (( Cl ( union G)) \/ ( Cl ( union (F \ G)))) by PRE_TOPC: 20;

        then a in ( Cl ( union (F \ G))) by A3, A6, A7, XBOOLE_0:def 3;

        then a in ( union ( clf (F \ G))) by A2, A8, A9, PCOMPS_1: 16;

        hence contradiction by A4, A10, XBOOLE_0:def 3;

      end;

      let a be object;

      assume

       A11: a in (( union ( clf F)) \/ ( meet Z));

      per cases by A11, XBOOLE_0:def 3;

        suppose a in ( union ( clf F));

        then

        consider b such that

         A12: a in b and

         A13: b in ( clf F) by TARSKI:def 4;

        ex W be Subset of T st b = ( Cl W) & W in F by A13, PCOMPS_1:def 2;

        then b c= ( Cl ( union F)) by PRE_TOPC: 19, ZFMISC_1: 74;

        hence thesis by A12;

      end;

        suppose

         A14: a in ( meet Z9);

        ( union G0) c= ( union F) by ZFMISC_1: 77;

        then

         A15: ( Cl ( union G0)) c= ( Cl ( union F)) by PRE_TOPC: 19;

        a in ( Cl ( union G0)) by A1, A14, SETFAM_1:def 1;

        hence thesis by A15;

      end;

    end;

    theorem :: TOPGEN_2:37

    for T be TopSpace, F be Subset-Family of T holds ( Cl ( union F)) = (( union ( clf F)) \/ ( meet { ( Cl ( union G)) where G be Subset-Family of T : G c= F & (F \ G) is finite }))

    proof

      let T be TopSpace;

      let F be Subset-Family of T;

      set Z = { ( Cl ( union G)) where G be Subset-Family of T : G c= F & (F \ G) is finite };

      (F \ F) = {} by XBOOLE_1: 37;

      then

       A1: ( Cl ( union F)) in Z;

      then

      reconsider Z9 = Z as non empty set;

      thus ( Cl ( union F)) c= (( union ( clf F)) \/ ( meet Z))

      proof

        let a be object;

        assume that

         A2: a in ( Cl ( union F)) and

         A3: not a in (( union ( clf F)) \/ ( meet Z));

        reconsider a as Point of T by A2;

         not a in ( meet Z9) by A3, XBOOLE_0:def 3;

        then

        consider b such that

         A4: b in Z and

         A5: not a in b by SETFAM_1:def 1;

        consider G be Subset-Family of T such that

         A6: b = ( Cl ( union G)) and

         A7: G c= F and

         A8: (F \ G) is finite by A4;



         A9: T is non empty by A2;

        then ( clf (F \ G)) c= ( clf F) by PCOMPS_1: 14, XBOOLE_1: 36;

        then

         A10: ( union ( clf (F \ G))) c= ( union ( clf F)) by ZFMISC_1: 77;

        F = (G \/ (F \ G)) by A7, XBOOLE_1: 45;

        then ( union F) = (( union G) \/ ( union (F \ G))) by ZFMISC_1: 78;

        then ( Cl ( union F)) = (( Cl ( union G)) \/ ( Cl ( union (F \ G)))) by PRE_TOPC: 20;

        then a in ( Cl ( union (F \ G))) by A2, A5, A6, XBOOLE_0:def 3;

        then a in ( union ( clf (F \ G))) by A8, A9, PCOMPS_1: 16;

        hence contradiction by A3, A10, XBOOLE_0:def 3;

      end;

      let a be object;

      assume

       A11: a in (( union ( clf F)) \/ ( meet Z));

      per cases by A11, XBOOLE_0:def 3;

        suppose a in ( union ( clf F));

        then

        consider b such that

         A12: a in b and

         A13: b in ( clf F) by TARSKI:def 4;

        ex W be Subset of T st b = ( Cl W) & W in F by A13, PCOMPS_1:def 2;

        then b c= ( Cl ( union F)) by PRE_TOPC: 19, ZFMISC_1: 74;

        hence thesis by A12;

      end;

        suppose a in ( meet Z9);

        hence thesis by A1, SETFAM_1:def 1;

      end;

    end;

    theorem :: TOPGEN_2:38

    for X be set, O be Subset-Family of ( bool X) st for o be Subset-Family of X st o in O holds TopStruct (# X, o #) is TopSpace holds ex B be Subset-Family of X st B = ( Intersect O) & TopStruct (# X, B #) is TopSpace & (for o be Subset-Family of X st o in O holds TopStruct (# X, o #) is TopExtension of TopStruct (# X, B #)) & for T be TopSpace st the carrier of T = X & for o be Subset-Family of X st o in O holds TopStruct (# X, o #) is TopExtension of T holds TopStruct (# X, B #) is TopExtension of T

    proof

      let X be set;

      let O be Subset-Family of ( bool X) such that

       A1: for o be Subset-Family of X st o in O holds TopStruct (# X, o #) is TopSpace;

      reconsider B = ( Intersect O) as Subset-Family of X;

      set T = TopStruct (# X, B #);

      take B;

      thus B = ( Intersect O);



       A2: T is TopSpace-like

      proof

        now

          thus the carrier of T in ( bool the carrier of T) by ZFMISC_1:def 1;

          let a;

          assume

           A3: a in O;

          then

          reconsider o = a as Subset-Family of X;

           TopStruct (# X, o #) is TopSpace by A1, A3;

          hence the carrier of T in a by PRE_TOPC:def 1;

        end;

        hence the carrier of T in the topology of T by SETFAM_1: 43;

        hereby

          let a be Subset-Family of T such that

           A4: a c= the topology of T;

          now

            let b;

            assume

             A5: b in O;

            then

            reconsider o = b as Subset-Family of X;

            B c= b by A5, MSSUBFAM: 2;

            then

             A6: a c= o by A4;

             TopStruct (# X, o #) is TopSpace by A1, A5;

            hence ( union a) in b by A6, PRE_TOPC:def 1;

          end;

          hence ( union a) in the topology of T by SETFAM_1: 43;

        end;

        let a,b be Subset of T such that

         A7: a in the topology of T and

         A8: b in the topology of T;

        now

          let c;

          assume

           A9: c in O;

          then

          reconsider o = c as Subset-Family of X;



           A10: b in o by A8, A9, SETFAM_1: 43;



           A11: TopStruct (# X, o #) is TopSpace by A1, A9;

          a in o by A7, A9, SETFAM_1: 43;

          hence (a /\ b) in c by A10, A11, PRE_TOPC:def 1;

        end;

        hence thesis by SETFAM_1: 43;

      end;

      hence T is TopSpace;

      thus for o be Subset-Family of X st o in O holds TopStruct (# X, o #) is TopExtension of T

      proof

        let o be Subset-Family of X such that

         A12: o in O;

        reconsider S = TopStruct (# X, o #) as TopSpace by A1, A12;

        ( Intersect O) c= o by A12, MSSUBFAM: 2;

        then S is TopExtension of T by YELLOW_9:def 5;

        hence thesis;

      end;

      reconsider TT = T as TopSpace by A2;

      let T9 be TopSpace such that

       A13: the carrier of T9 = X and

       A14: for o be Subset-Family of X st o in O holds TopStruct (# X, o #) is TopExtension of T9;

      now

        let a;

        assume

         A15: a in O;

        then

        reconsider o = a as Subset-Family of X;

         TopStruct (# X, o #) is TopExtension of T9 by A14, A15;

        hence the topology of T9 c= a by YELLOW_9:def 5;

      end;

      then the topology of T9 c= ( Intersect O) by A13, MSSUBFAM: 4;

      then TT is TopExtension of T9 by A13, YELLOW_9:def 5;

      hence thesis;

    end;

    theorem :: TOPGEN_2:39

    for X be set, O be Subset-Family of ( bool X) holds ex B be Subset-Family of X st B = ( UniCl ( FinMeetCl ( union O))) & TopStruct (# X, B #) is TopSpace & (for o be Subset-Family of X st o in O holds TopStruct (# X, B #) is TopExtension of TopStruct (# X, o #)) & for T be TopSpace st the carrier of T = X & for o be Subset-Family of X st o in O holds T is TopExtension of TopStruct (# X, o #) holds T is TopExtension of TopStruct (# X, B #)

    proof

      reconsider e = ( {} ( bool {} )), tE = {( {} {} )} as Subset-Family of {} ;

      reconsider E = ( {} ( bool ( bool {} ))) as empty Subset-Family of ( bool {} );

      let X be set;

      let O be Subset-Family of ( bool X);

      reconsider B = ( UniCl ( FinMeetCl ( union O))) as Subset-Family of X;

      take B;

      thus B = ( UniCl ( FinMeetCl ( union O)));

      reconsider dT = TopStruct (# {} , tE #) as discrete TopStruct by TDLAT_3:def 1, ZFMISC_1: 1;



       A1: { {} , {} } = tE by ENUMSET1: 29;



       A2: ( FinMeetCl tE) = { {} , {} } by YELLOW_9: 11;

       A3:

      now

        assume

         A4: X is empty;

        hence

         A5: ( union O) = e or ( union O) = tE by ZFMISC_1: 1, ZFMISC_1: 33;

        thus ( FinMeetCl ( union E)) = the topology of dT by YELLOW_9: 17;

        hence TopStruct (# X, B #) is TopSpace by A2, A1, A4, A5, YELLOW_9: 11;

      end;

      hence TopStruct (# X, B #) is TopSpace by CANTOR_1: 15;

      reconsider TT = TopStruct (# X, B #) as TopSpace by A3, CANTOR_1: 15;

      hereby

        let o be Subset-Family of X;

        set S = TopStruct (# X, o #);



         A6: ( FinMeetCl ( union O)) c= B by CANTOR_1: 1;

        assume o in O;

        then

         A7: o c= ( union O) by ZFMISC_1: 74;

        ( union O) c= ( FinMeetCl ( union O)) by CANTOR_1: 4;

        then o c= ( FinMeetCl ( union O)) by A7;

        then the topology of S c= the topology of TT by A6;

        hence TopStruct (# X, B #) is TopExtension of S by YELLOW_9:def 5;

      end;

      let T be TopSpace such that

       A8: the carrier of T = X and

       A9: for o be Subset-Family of X st o in O holds T is TopExtension of TopStruct (# X, o #);

      thus the carrier of T = the carrier of TopStruct (# X, B #) by A8;



       A10: X <> {} implies T is non empty by A8;

      now

        let a;

        assume

         A11: a in O;

        then

        reconsider o = a as Subset-Family of X;

        T is TopExtension of TopStruct (# X, o #) by A9, A11;

        hence a c= the topology of T by YELLOW_9:def 5;

      end;

      then ( union O) c= the topology of T by ZFMISC_1: 76;

      then ( FinMeetCl ( union O)) c= ( FinMeetCl the topology of T) by A8, CANTOR_1: 14;

      then

       A12: B c= ( UniCl ( FinMeetCl the topology of T)) by A8, CANTOR_1: 9;

      X in the topology of T by A8, PRE_TOPC:def 1;

      hence thesis by A12, A10, CANTOR_1: 7;

    end;