yellow_8.miz

    begin

    theorem :: YELLOW_8:1



     Th1: for X,A,B be set st A in ( Fin X) & B c= A holds B in ( Fin X)

    proof

      let X,A,B be set such that

       A1: A in ( Fin X) and

       A2: B c= A;

      A c= X by A1, FINSUB_1:def 5;

      then B c= X by A2;

      hence thesis by A1, A2, FINSUB_1:def 5;

    end;

    theorem :: YELLOW_8:2



     Th2: for X be set, F be Subset-Family of X st F c= ( Fin X) holds ( meet F) in ( Fin X)

    proof

      let X be set, F be Subset-Family of X such that

       A1: F c= ( Fin X);

      per cases ;

        suppose F = {} ;

        hence thesis by FINSUB_1: 7, SETFAM_1: 1;

      end;

        suppose F <> {} ;

        then

        consider A be object such that

         A2: A in F by XBOOLE_0:def 1;

        reconsider A as set by TARSKI: 1;

        ( meet F) c= A by A2, SETFAM_1: 3;

        hence thesis by A1, A2, Th1;

      end;

    end;

    begin

    theorem :: YELLOW_8:3



     Th3: for X be set, F be Subset-Family of X holds (F,( COMPLEMENT F)) are_equipotent

    proof

      let X be set, F be Subset-Family of X;

      deffunc F( set) = (X \ $1);

      consider f be Function such that

       A1: ( dom f) = F and

       A2: for x be set st x in F holds (f . x) = F(x) from FUNCT_1:sch 5;

      take f;

      thus f is one-to-one

      proof

        let x1,x2 be object such that

         A3: x1 in ( dom f) and

         A4: x2 in ( dom f) and

         A5: (f . x1) = (f . x2);

        reconsider X1 = x1, X2 = x2 as Subset of X by A1, A3, A4;

        (X1 ` ) = (f . x1) by A1, A2, A3

        .= (X2 ` ) by A1, A2, A4, A5;



        hence x1 = ((X2 ` ) ` )

        .= x2;

      end;

      thus ( dom f) = F by A1;

      thus ( rng f) c= ( COMPLEMENT F)

      proof

        let e be object;

        assume e in ( rng f);

        then

        consider u be object such that

         A6: u in ( dom f) and

         A7: e = (f . u) by FUNCT_1:def 3;

        reconsider Y = u as Subset of X by A1, A6;

        e = (Y ` ) by A1, A2, A6, A7;

        hence thesis by A1, A6, SETFAM_1: 35;

      end;

      let e be object;

      assume

       A8: e in ( COMPLEMENT F);

      then

      reconsider Y = e as Subset of X;



       A9: (Y ` ) in F by A8, SETFAM_1:def 7;

      e = ((Y ` ) ` )

      .= (f . (Y ` )) by A2, A9;

      hence thesis by A1, A9, FUNCT_1:def 3;

    end;

    theorem :: YELLOW_8:4



     Th4: for X,Y be set st (X,Y) are_equipotent & X is countable holds Y is countable

    proof

      let X,Y be set;

      assume (X,Y) are_equipotent & ( card X) c= omega ;

      hence ( card Y) c= omega by CARD_1: 5;

    end;

    theorem :: YELLOW_8:5

    for X be 1-sorted, F be Subset-Family of X, P be Subset of X holds (P ` ) in ( COMPLEMENT F) iff P in F

    proof

      let X be 1-sorted, F be Subset-Family of X, P be Subset of X;

      P = ((P ` ) ` );

      hence thesis by SETFAM_1:def 7;

    end;

    theorem :: YELLOW_8:6



     Th6: for X be 1-sorted, F be Subset-Family of X holds ( Intersect ( COMPLEMENT F)) = (( union F) ` )

    proof

      let X be 1-sorted, F be Subset-Family of X;

      per cases ;

        suppose

         A1: F <> {} ;

        then ( COMPLEMENT F) <> {} by SETFAM_1: 32;



        hence ( Intersect ( COMPLEMENT F)) = ( meet ( COMPLEMENT F)) by SETFAM_1:def 9

        .= (( [#] the carrier of X) \ ( union F)) by A1, SETFAM_1: 33

        .= (( union F) ` );

      end;

        suppose F = {} ;

        then

        reconsider G = F as empty Subset-Family of X;

        ( COMPLEMENT G) = {} ;

        hence thesis by SETFAM_1:def 9, ZFMISC_1: 2;

      end;

    end;

    theorem :: YELLOW_8:7



     Th7: for X be 1-sorted, F be Subset-Family of X holds ( union ( COMPLEMENT F)) = (( Intersect F) ` )

    proof

      let X be 1-sorted, F be Subset-Family of X;



      thus ( union ( COMPLEMENT F)) = ((( union ( COMPLEMENT F)) ` ) ` )

      .= (( Intersect ( COMPLEMENT ( COMPLEMENT F))) ` ) by Th6

      .= (( Intersect F) ` );

    end;

    begin

    theorem :: YELLOW_8:8

    for T be non empty TopSpace, A,B be Subset of T st B c= A & A is closed & (for C be Subset of T st B c= C & C is closed holds A c= C) holds A = ( Cl B) by PRE_TOPC: 18, TOPS_1: 5;

    theorem :: YELLOW_8:9



     Th9: for T be TopStruct, B be Basis of T, V be Subset of T st V is open holds V = ( union { G where G be Subset of T : G in B & G c= V })

    proof

      let T be TopStruct, B be Basis of T, V be Subset of T such that

       A1: V is open;

      set X = { G where G be Subset of T : G in B & G c= V };



       A2: the topology of T c= ( UniCl B) by CANTOR_1:def 2;

      for x be object holds x in V iff ex Y be set st x in Y & Y in X

      proof

        let x be object;

        hereby

          V in the topology of T by A1;

          then

          consider Y be Subset-Family of T such that

           A3: Y c= B and

           A4: V = ( union Y) by A2, CANTOR_1:def 1;

          assume x in V;

          then

          consider W be set such that

           A5: x in W and

           A6: W in Y by A4, TARSKI:def 4;

          take W;

          thus x in W by A5;

          reconsider G = W as Subset of T by A6;

          G c= V by A4, A6, ZFMISC_1: 74;

          hence W in X by A3, A6;

        end;

        given Y be set such that

         A7: x in Y and

         A8: Y in X;

        ex G be Subset of T st Y = G & G in B & G c= V by A8;

        hence thesis by A7;

      end;

      hence thesis by TARSKI:def 4;

    end;

    theorem :: YELLOW_8:10



     Th10: for T be TopStruct, B be Basis of T, S be Subset of T st S in B holds S is open

    proof

      let T be TopStruct, B be Basis of T, S be Subset of T such that

       A1: S in B;

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

      hence thesis by A1;

    end;

    theorem :: YELLOW_8:11

    for T be non empty TopSpace, B be Basis of T, V be Subset of T holds ( Int V) = ( union { G where G be Subset of T : G in B & G c= V })

    proof

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

      set X = { G where G be Subset of T : G in B & G c= V }, Y = { G where G be Subset of T : G in B & G c= ( Int V) };

      X = Y

      proof

        thus X c= Y

        proof

          let e be object;

          assume e in X;

          then

          consider G be Subset of T such that

           A1: e = G and

           A2: G in B and

           A3: G c= V;

          G c= ( Int V) by A2, A3, Th10, TOPS_1: 24;

          hence thesis by A1, A2;

        end;

        let e be object;

        assume e in Y;

        then

        consider G be Subset of T such that

         A4: e = G & G in B and

         A5: G c= ( Int V);

        ( Int V) c= V by TOPS_1: 16;

        then G c= V by A5;

        hence thesis by A4;

      end;

      hence thesis by Th9;

    end;

    begin

    definition

      let T be non empty TopStruct, x be Point of T, F be Subset-Family of T;

      :: YELLOW_8:def1

      attr F is x -quasi_basis means

      : Def1: x in ( Intersect F) & for S be Subset of T st S is open & x in S holds ex V be Subset of T st V in F & V c= S;

    end

    registration

      let T be non empty TopStruct, x be Point of T;

      cluster openx -quasi_basis for Subset-Family of T;

      existence

      proof

        defpred P[ set] means $1 in the topology of T & x in $1;

        set IT = { S where S be Subset of T : P[S] };

        IT is Subset-Family of T from DOMAIN_1:sch 7;

        then

        reconsider IT as Subset-Family of T;

        take IT;

        IT c= the topology of T

        proof

          let e be object;

          assume e in IT;

          then ex S be Subset of T st S = e & S in the topology of T & x in S;

          hence thesis;

        end;

        hence IT is open by TOPS_2: 64;

        now

          let e be set;

          assume e in IT;

          then ex S be Subset of T st S = e & S in the topology of T & x in S;

          hence x in e;

        end;

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

        let S be Subset of T such that

         A1: S is open and

         A2: x in S;

        take V = S;

        V in the topology of T by A1;

        hence V in IT by A2;

        thus thesis;

      end;

    end

    definition

      let T be non empty TopStruct, x be Point of T;

      mode Basis of x is openx -quasi_basis Subset-Family of T;

    end

    theorem :: YELLOW_8:12



     Th12: for T be non empty TopStruct, x be Point of T, B be Basis of x, V be Subset of T st V in B holds V is open & x in V

    proof

      let T be non empty TopStruct, x be Point of T, B be Basis of x, V be Subset of T such that

       A1: V in B;

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

      hence V is open by A1;

      x in ( Intersect B) by Def1;

      hence thesis by A1, SETFAM_1: 43;

    end;

    theorem :: YELLOW_8:13

    for T be non empty TopStruct, x be Point of T, B be Basis of x, V be Subset of T st x in V & V is open holds ex W be Subset of T st W in B & W c= V by Def1;

    theorem :: YELLOW_8:14

    for T be non empty TopStruct, P be Subset-Family of T st P c= the topology of T & for x be Point of T holds ex B be Basis of x st B c= P holds P is Basis of T

    proof

      let T be non empty TopStruct;

      let P be Subset-Family of T such that

       A1: P c= the topology of T and

       A2: for x be Point of T holds ex B be Basis of x st B c= P;

      P is quasi_basis

      proof

        let e be object;

        assume

         A3: e in the topology of T;

        then

        reconsider S = e as Subset of T;

        set X = { V where V be Subset of T : V in P & V c= S };



         A4: X c= P

        proof

          let e be object;

          assume e in X;

          then ex V be Subset of T st e = V & V in P & V c= S;

          hence thesis;

        end;

        then

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

        for u be object holds u in S iff ex Z be set st u in Z & Z in X

        proof

          let u be object;

          hereby

            assume

             A5: u in S;

            then

            reconsider p = u as Point of T;

            consider B be Basis of p such that

             A6: B c= P by A2;

            S is open by A3;

            then

            consider W be Subset of T such that

             A7: W in B and

             A8: W c= S by A5, Def1;

            reconsider Z = W as set;

            take Z;

            thus u in Z by A7, Th12;

            thus Z in X by A6, A7, A8;

          end;

          given Z be set such that

           A9: u in Z and

           A10: Z in X;

          ex V be Subset of T st V = Z & V in P & V c= S by A10;

          hence thesis by A9;

        end;

        then S = ( union X) by TARSKI:def 4;

        hence thesis by A4, CANTOR_1:def 1;

      end;

      hence thesis by A1, TOPS_2: 64;

    end;

    definition

      let T be non empty TopSpace;

      :: YELLOW_8:def2

      attr T is Baire means for F be Subset-Family of T st F is countable & for S be Subset of T st S in F holds S is everywhere_dense holds ex I be Subset of T st I = ( Intersect F) & I is dense;

    end

    theorem :: YELLOW_8:15

    for T be non empty TopSpace holds T is Baire iff for F be Subset-Family of T st F is countable & for S be Subset of T st S in F holds S is nowhere_dense holds ( union F) is boundary

    proof

      let T be non empty TopSpace;

      hereby

        assume

         A1: T is Baire;

        let F be Subset-Family of T such that

         A2: F is countable and

         A3: for S be Subset of T st S in F holds S is nowhere_dense;

        reconsider G = ( COMPLEMENT F) as Subset-Family of T;



         A4: for S be Subset of T st S in G holds S is everywhere_dense

        proof

          let S be Subset of T;

          assume S in G;

          then (S ` ) in F by SETFAM_1:def 7;

          then (S ` ) is nowhere_dense by A3;

          hence thesis by TOPS_3: 39;

        end;

        G is countable by A2, Th3, Th4;

        then ex I be Subset of T st I = ( Intersect G) & I is dense by A1, A4;

        then (( union F) ` ) is dense by Th6;

        hence ( union F) is boundary by TOPS_1:def 4;

      end;

      assume

       A5: for F be Subset-Family of T st F is countable & for S be Subset of T st S in F holds S is nowhere_dense holds ( union F) is boundary;

      let F be Subset-Family of T such that

       A6: F is countable and

       A7: for S be Subset of T st S in F holds S is everywhere_dense;

      reconsider I = ( Intersect F) as Subset of T;

      take I;

      thus I = ( Intersect F);

      reconsider G = ( COMPLEMENT F) as Subset-Family of T;



       A8: for S be Subset of T st S in G holds S is nowhere_dense

      proof

        let S be Subset of T;

        assume S in G;

        then (S ` ) in F by SETFAM_1:def 7;

        then (S ` ) is everywhere_dense by A7;

        hence thesis by TOPS_3: 40;

      end;

      G is countable by A6, Th3, Th4;

      then ( union G) is boundary by A5, A8;

      then (( Intersect F) ` ) is boundary by Th7;

      hence thesis by TOPS_3: 18;

    end;

    begin

    definition

      let T be TopStruct, S be Subset of T;

      :: YELLOW_8:def3

      attr S is irreducible means

      : Def3: S is non empty closed & for S1,S2 be Subset of T st S1 is closed & S2 is closed & S = (S1 \/ S2) holds S1 = S or S2 = S;

    end

    registration

      let T be TopStruct;

      cluster irreducible -> non empty for Subset of T;

      coherence ;

    end

    definition

      let T be non empty TopSpace, S be Subset of T;

      let p be Point of T;

      :: YELLOW_8:def4

      pred p is_dense_point_of S means p in S & S c= ( Cl {p});

    end

    theorem :: YELLOW_8:16

    for T be non empty TopSpace, S be Subset of T st S is closed holds for p be Point of T st p is_dense_point_of S holds S = ( Cl {p}) by ZFMISC_1: 31, TOPS_1: 5;

    theorem :: YELLOW_8:17



     Th17: for T be non empty TopSpace, p be Point of T holds ( Cl {p}) is irreducible

    proof

      let T be non empty TopSpace, p be Point of T;

      assume

       A1: not thesis;

      ( Cl {p}) is non empty by PCOMPS_1: 2;

      then

      consider S1,S2 be Subset of T such that

       A2: S1 is closed & S2 is closed and

       A3: ( Cl {p}) = (S1 \/ S2) and

       A4: S1 <> ( Cl {p}) & S2 <> ( Cl {p}) by A1;

       {p} c= ( Cl {p}) & p in {p} by PRE_TOPC: 18, TARSKI:def 1;

      then p in S1 or p in S2 by A3, XBOOLE_0:def 3;

      then {p} c= S1 or {p} c= S2 by ZFMISC_1: 31;

      then

       A5: ( Cl {p}) c= S1 or ( Cl {p}) c= S2 by A2, TOPS_1: 5;

      S1 c= ( Cl {p}) & S2 c= ( Cl {p}) by A3, XBOOLE_1: 7;

      hence contradiction by A4, A5;

    end;

    registration

      let T be non empty TopSpace;

      cluster irreducible for Subset of T;

      existence

      proof

        set p = the Point of T;

        ( Cl {p}) is irreducible by Th17;

        hence thesis;

      end;

    end

    definition

      let T be non empty TopSpace;

      :: YELLOW_8:def5

      attr T is sober means

      : Def5: for S be irreducible Subset of T holds ex p be Point of T st p is_dense_point_of S & for q be Point of T st q is_dense_point_of S holds p = q;

    end

    theorem :: YELLOW_8:18



     Th18: for T be non empty TopSpace, p be Point of T holds p is_dense_point_of ( Cl {p})

    proof

      let T be non empty TopSpace, p be Point of T;

       {p} c= ( Cl {p}) & p in {p} by PRE_TOPC: 18, TARSKI:def 1;

      hence p in ( Cl {p});

      thus thesis;

    end;

    theorem :: YELLOW_8:19



     Th19: for T be non empty TopSpace, p be Point of T holds p is_dense_point_of {p} by TARSKI:def 1, PRE_TOPC: 18;

    theorem :: YELLOW_8:20



     Th20: for T be non empty TopSpace, G,F be Subset of T st G is open & F is closed holds (F \ G) is closed

    proof

      let T be non empty TopSpace, G,F be Subset of T such that

       A1: G is open & F is closed;

      (F \ G) = (F /\ (G ` )) by SUBSET_1: 13;

      hence thesis by A1;

    end;

    theorem :: YELLOW_8:21



     Th21: for T be Hausdorff non empty TopSpace, S be irreducible Subset of T holds S is trivial

    proof

      let T be Hausdorff non empty TopSpace, S be irreducible Subset of T;

      assume S is non trivial;

      then

      consider x,y be Point of T such that

       A1: x in S & y in S and

       A2: x <> y by SUBSET_1: 45;

      consider W,V be Subset of T such that

       A3: W is open & V is open and

       A4: x in W & y in V and

       A5: W misses V by A2, PRE_TOPC:def 10;

      set S1 = (S \ W), S2 = (S \ V);



       A6: S1 <> S & S2 <> S by A4, A1, XBOOLE_0:def 5;

      S is closed by Def3;

      then

       A7: S1 is closed & S2 is closed by A3, Th20;



       A8: (W /\ V) = {} by A5;

      (S1 \/ S2) = (S \ (W /\ V)) by XBOOLE_1: 54

      .= S by A8;

      hence contradiction by A7, A6, Def3;

    end;

    registration

      let T be Hausdorff non empty TopSpace;

      cluster irreducible -> trivial for Subset of T;

      coherence by Th21;

    end

    theorem :: YELLOW_8:22



     Th22: for T be Hausdorff non empty TopSpace holds T is sober

    proof

      let T be Hausdorff non empty TopSpace;

      let S be irreducible Subset of T;

      consider d be Element of S such that

       A1: S = {d} by SUBSET_1: 46;

      reconsider d as Point of T;

      take d;

      thus d is_dense_point_of S by A1, Th19;

      let p be Point of T;

      assume p is_dense_point_of S;

      then p in S;

      hence thesis by A1, TARSKI:def 1;

    end;

    registration

      cluster Hausdorff -> sober for non empty TopSpace;

      coherence by Th22;

    end

    registration

      cluster sober for non empty TopSpace;

      existence

      proof

        set T = the Hausdorff non empty TopSpace;

        take T;

        thus thesis;

      end;

    end

    theorem :: YELLOW_8:23



     Th23: for T be non empty TopSpace holds T is T_0 iff for p,q be Point of T st ( Cl {p}) = ( Cl {q}) holds p = q

    proof

      let T be non empty TopSpace;

      thus T is T_0 implies for p,q be Point of T st ( Cl {p}) = ( Cl {q}) holds p = q by TSP_1:def 5;

      assume for p,q be Point of T st ( Cl {p}) = ( Cl {q}) holds p = q;

      then for p,q be Point of T st p <> q holds ( Cl {p}) <> ( Cl {q});

      hence thesis by TSP_1:def 5;

    end;

    theorem :: YELLOW_8:24



     Th24: for T be sober non empty TopSpace holds T is T_0

    proof

      let T be sober non empty TopSpace;

      for p,q be Point of T st ( Cl {p}) = ( Cl {q}) holds p = q

      proof

        let p,q be Point of T such that

         A1: ( Cl {p}) = ( Cl {q});

        ( Cl {p}) is irreducible by Th17;

        then

        consider r be Point of T such that r is_dense_point_of ( Cl {p}) and

         A2: for q be Point of T st q is_dense_point_of ( Cl {p}) holds r = q by Def5;

        p = r by A2, Th18;

        hence thesis by A1, A2, Th18;

      end;

      hence thesis by Th23;

    end;

    registration

      cluster sober -> T_0 for non empty TopSpace;

      coherence by Th24;

    end

    definition

      let X be set;

      :: YELLOW_8:def6

      func CofinTop X -> strict TopStruct means

      : Def6: the carrier of it = X & ( COMPLEMENT the topology of it ) = ( {X} \/ ( Fin X));

      existence

      proof

         {X} c= ( bool X) & ( Fin X) c= ( bool X) by FINSUB_1: 13, ZFMISC_1: 68;

        then

        reconsider F = ( {X} \/ ( Fin X)) as Subset-Family of X by XBOOLE_1: 8;

        reconsider F as Subset-Family of X;

        take T = TopStruct (# X, ( COMPLEMENT F) #);

        thus the carrier of T = X;

        thus thesis;

      end;

      uniqueness by SETFAM_1: 38;

    end

    registration

      let X be non empty set;

      cluster ( CofinTop X) -> non empty;

      coherence by Def6;

    end

    registration

      let X be set;

      cluster ( CofinTop X) -> TopSpace-like;

      coherence

      proof

        reconsider F = ( Fin X) as Subset-Family of X by FINSUB_1: 13;

        reconsider XX = {X} as Subset-Family of X by ZFMISC_1: 68;

        set IT = ( CofinTop X);

        reconsider XX as Subset-Family of X;

        reconsider F as Subset-Family of X;



         A1: the carrier of IT = X by Def6;



         A2: ( COMPLEMENT the topology of IT) = ( {X} \/ ( Fin X)) by Def6;



         A3: the topology of IT = ( COMPLEMENT ( COMPLEMENT the topology of IT))

        .= (( COMPLEMENT XX) \/ ( COMPLEMENT F)) by A1, A2, SETFAM_1: 39

        .= ( { {} } \/ ( COMPLEMENT F)) by SETFAM_1: 40;

        ( {}. X) in F;

        then ((( {} X) ` ) ` ) in F;

        then ( [#] X) in ( COMPLEMENT F) by SETFAM_1:def 7;

        hence the carrier of IT in the topology of IT by A1, A3, XBOOLE_0:def 3;



         A4: {} in { {} } by TARSKI:def 1;

        thus for a be Subset-Family of IT st a c= the topology of IT holds ( union a) in the topology of IT

        proof

          let a be Subset-Family of IT such that

           A5: a c= the topology of IT;

          set b = (a /\ ( COMPLEMENT F));

          reconsider b as Subset-Family of X;

          reconsider b as Subset-Family of X;

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

          then (a /\ { {} }) = { {} } or (a /\ { {} }) = {} by ZFMISC_1: 33;

          then

           A6: ( union (a /\ { {} })) = {} by ZFMISC_1: 2, ZFMISC_1: 25;



           A7: ( union a) = ( union (a /\ the topology of IT)) by A5, XBOOLE_1: 28

          .= ( union ((a /\ { {} }) \/ (a /\ ( COMPLEMENT F)))) by A3, XBOOLE_1: 23

          .= (( union (a /\ { {} })) \/ ( union (a /\ ( COMPLEMENT F)))) by ZFMISC_1: 78

          .= ( union b) by A6;

          per cases ;

            suppose b = {} ;

            hence thesis by A3, A4, A7, XBOOLE_0:def 3, ZFMISC_1: 2;

          end;

            suppose

             A8: b <> {} ;

            b c= ( COMPLEMENT F) by XBOOLE_1: 17;

            then

             A9: ( COMPLEMENT b) c= ( Fin X) by SETFAM_1: 37;

            ( meet ( COMPLEMENT b)) = (( [#] X) \ ( union b)) by A8, SETFAM_1: 33

            .= (( union b) ` );

            then (( union b) ` ) in ( Fin X) by A9, Th2;

            then ( union b) in ( COMPLEMENT F) by SETFAM_1:def 7;

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

          end;

        end;

        let a,b be Subset of IT such that

         A10: a in the topology of IT and

         A11: b in the topology of IT;

        reconsider a9 = a, b9 = b as Subset of X by Def6;

        per cases ;

          suppose a = {} or b = {} ;

          hence (a /\ b) in the topology of IT by A3, A4, XBOOLE_0:def 3;

        end;

          suppose

           A12: a <> {} & b <> {} ;

          then not b in { {} } by TARSKI:def 1;

          then b9 in ( COMPLEMENT F) by A3, A11, XBOOLE_0:def 3;

          then

           A13: (b9 ` ) in ( Fin X) by SETFAM_1:def 7;

           not a in { {} } by A12, TARSKI:def 1;

          then a9 in ( COMPLEMENT F) by A3, A10, XBOOLE_0:def 3;

          then (a9 ` ) in ( Fin X) by SETFAM_1:def 7;

          then ((a9 ` ) \/ (b9 ` )) in ( Fin X) by A13, FINSUB_1: 1;

          then ((a9 /\ b9) ` ) in ( Fin X) by XBOOLE_1: 54;

          then (a /\ b) in ( COMPLEMENT F) by SETFAM_1:def 7;

          hence (a /\ b) in the topology of IT by A3, XBOOLE_0:def 3;

        end;

      end;

    end

    theorem :: YELLOW_8:25



     Th25: for X be non empty set, P be Subset of ( CofinTop X) holds P is closed iff P = X or P is finite

    proof

      let X be non empty set, P be Subset of ( CofinTop X);

      set T = ( CofinTop X);

      hereby

        assume that

         A1: P is closed and

         A2: P <> X;

        (P ` ) in the topology of T by A1, PRE_TOPC:def 2;

        then P in ( COMPLEMENT the topology of T) by SETFAM_1:def 7;

        then

         A3: P in ( {X} \/ ( Fin X)) by Def6;

         not P in {X} by A2, TARSKI:def 1;

        then P in ( Fin X) by A3, XBOOLE_0:def 3;

        hence P is finite;

      end;

      assume

       A4: P = X or P is finite;

      the carrier of T = X by Def6;

      then P in {X} or P in ( Fin X) by A4, FINSUB_1:def 5, TARSKI:def 1;

      then P in ( {X} \/ ( Fin X)) by XBOOLE_0:def 3;

      then P in ( COMPLEMENT the topology of T) by Def6;

      then (P ` ) in the topology of T by SETFAM_1:def 7;

      then (P ` ) is open;

      hence thesis;

    end;

    theorem :: YELLOW_8:26



     Th26: for T be non empty TopSpace st T is T_1 holds for p be Point of T holds ( Cl {p}) = {p} by URYSOHN1: 19, TOPS_1: 5, PRE_TOPC: 18;

    registration

      let X be non empty set;

      cluster ( CofinTop X) -> T_1;

      coherence

      proof

        for p be Point of ( CofinTop X) holds {p} is closed by Th25;

        hence thesis by URYSOHN1: 19;

      end;

    end

    registration

      let X be infinite set;

      cluster ( CofinTop X) -> non sober;

      coherence

      proof

        set T = ( CofinTop X);

        reconsider S = ( [#] X) as Subset of T by Def6;

        S is irreducible

        proof

          X = ( [#] T) by Def6;

          hence S is non empty closed;

          let S1,S2 be Subset of T such that

           A1: S1 is closed & S2 is closed and

           A2: S = (S1 \/ S2);

          assume S1 <> S & S2 <> S;

          then

          reconsider S19 = S1, S29 = S2 as finite set by A1, Th25;

          S = (S19 \/ S29) by A2;

          hence contradiction;

        end;

        then

        reconsider S as irreducible Subset of T;

        take S;

        let p be Point of T;

        now

          assume p is_dense_point_of S;

          then S c= ( Cl {p});

          then ( Cl {p}) is infinite;

          hence contradiction by Th26;

        end;

        hence thesis;

      end;

    end

    registration

      cluster T_1 non sober for non empty TopSpace;

      existence

      proof

        set X = the infinite set;

        take ( CofinTop X);

        thus thesis;

      end;

    end

    begin

    theorem :: YELLOW_8:27



     Th27: for T be non empty TopSpace holds T is regular iff for p be Point of T, P be Subset of T st p in ( Int P) holds ex Q be Subset of T st Q is closed & Q c= P & p in ( Int Q)

    proof

      let T be non empty TopSpace;

      hereby

        assume

         A1: T is regular;

        let p be Point of T, P be Subset of T;

        assume p in ( Int P);

        then

         A2: p in ((( Int P) ` ) ` );

        per cases ;

          suppose

           A3: P = ( [#] T);

          take Q = ( [#] T);

          thus Q is closed;

          thus Q c= P by A3;

          ( Int Q) = Q by TOPS_1: 15;

          hence p in ( Int Q);

        end;

          suppose P <> ( [#] T);

          consider W,V be Subset of T such that

           A4: W is open and

           A5: V is open and

           A6: p in W and

           A7: (( Int P) ` ) c= V and

           A8: W misses V by A1, A2;



           A9: ( Int P) c= P by TOPS_1: 16;

          take Q = (V ` );

          thus Q is closed by A5;

          (( Int P) ` ) c= (Q ` ) by A7;

          then Q c= ( Int P) by SUBSET_1: 12;

          hence Q c= P by A9;

          W c= Q by A8, SUBSET_1: 23;

          then W c= ( Int Q) by A4, TOPS_1: 24;

          hence p in ( Int Q) by A6;

        end;

      end;

      assume

       A10: for p be Point of T, P be Subset of T st p in ( Int P) holds ex Q be Subset of T st Q is closed & Q c= P & p in ( Int Q);

      let p be Point of T, P be Subset of T such that P <> {} and

       A11: P is closed & p in (P ` );

      p in ( Int (P ` )) by A11, TOPS_1: 23;

      then

      consider Q be Subset of T such that

       A12: Q is closed and

       A13: Q c= (P ` ) and

       A14: p in ( Int Q) by A10;

      reconsider W = ( Int Q) as Subset of T;

      take W, V = (Q ` );

      thus W is open;

      thus V is open by A12;

      thus p in W by A14;

      ((P ` ) ` ) c= V by A13, SUBSET_1: 12;

      hence P c= V;

      Q misses V by XBOOLE_1: 79;

      hence thesis by TOPS_1: 16, XBOOLE_1: 63;

    end;

    theorem :: YELLOW_8:28

    for T be non empty TopSpace st T is regular holds T is locally-compact iff for x be Point of T holds ex Y be Subset of T st x in ( Int Y) & Y is compact

    proof

      let T be non empty TopSpace such that

       A1: T is regular;

      hereby

        assume

         A2: T is locally-compact;

        let x be Point of T;

        ex Y be Subset of T st x in ( Int Y) & Y c= ( [#] T) & Y is compact by A2;

        hence ex Y be Subset of T st x in ( Int Y) & Y is compact;

      end;

      assume

       A3: for x be Point of T holds ex Y be Subset of T st x in ( Int Y) & Y is compact;

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

      assume x in X & X is open;

      then

       A4: x in ( Int X) by TOPS_1: 23;

      consider Y be Subset of T such that

       A5: x in ( Int Y) and

       A6: Y is compact by A3;

      x in (( Int X) /\ ( Int Y)) by A5, A4, XBOOLE_0:def 4;

      then x in ( Int (X /\ Y)) by TOPS_1: 17;

      then

      consider Q be Subset of T such that

       A7: Q is closed and

       A8: Q c= (X /\ Y) and

       A9: x in ( Int Q) by A1, Th27;

      take Q;

      thus x in ( Int Q) by A9;

      (X /\ Y) c= X by XBOOLE_1: 17;

      hence Q c= X by A8;

      (X /\ Y) c= Y by XBOOLE_1: 17;

      hence thesis by A6, A7, A8, COMPTS_1: 9, XBOOLE_1: 1;

    end;