compact1.miz



    begin

    definition

      let X be TopSpace, P be Subset-Family of X;

      :: COMPACT1:def1

      attr P is compact means for U be Subset of X st U in P holds U is compact;

    end

    definition

      let X be TopSpace, U be Subset of X;

      :: COMPACT1:def2

      attr U is relatively-compact means

      : Def2: ( Cl U) is compact;

    end

    registration

      let X be TopSpace;

      cluster empty -> relatively-compact for Subset of X;

      coherence by PRE_TOPC: 22;

    end

    registration

      let T be TopSpace;

      cluster relatively-compact for Subset of T;

      existence

      proof

        take ( {} T);

        thus thesis;

      end;

    end

    registration

      let X be TopSpace, U be relatively-compact Subset of X;

      cluster ( Cl U) -> compact;

      coherence by Def2;

    end

    notation

      let X be TopSpace, U be Subset of X;

      synonym U is pre-compact for U is relatively-compact;

    end

    notation

      let X be non empty TopSpace;

      synonym X is liminally-compact for X is locally-compact;

    end

    definition

      let X be non empty TopSpace;

      :: original: liminally-compact

      redefine

      :: COMPACT1:def3

      attr X is liminally-compact means

      : Def3: for x be Point of X holds ex B be basis of x st B is compact;

      compatibility

      proof

        hereby

          assume

           A1: X is liminally-compact;

          let x be Point of X;

          set B = { Q where Q be a_neighborhood of x : Q is compact & ex V be a_neighborhood of x st Q c= V };

          B c= ( bool ( [#] X))

          proof

            let A be object;

            assume A in B;

            then ex Q be a_neighborhood of x st A = Q & Q is compact & ex V be a_neighborhood of x st Q c= V;

            hence thesis;

          end;

          then

          reconsider B as Subset-Family of X;

          

           A2: B is basis of x

          proof

            let V be a_neighborhood of x;

            x in ( Int V) by CONNSP_2:def 1;

            then

            consider Q be Subset of X such that

             A3: x in ( Int Q) and

             A4: Q c= ( Int V) and

             A5: Q is compact by A1;

            reconsider Q as a_neighborhood of x by A3, CONNSP_2:def 1;

            take Q;

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

            hence thesis by A4, A5;

          end;

          B is compact

          proof

            let U be Subset of X;

            assume U in B;

            then ex Q be a_neighborhood of x st U = Q & Q is compact & ex V be a_neighborhood of x st Q c= V;

            hence thesis;

          end;

          hence ex B be basis of x st B is compact by A2;

        end;

        assume

         A6: for x be Point of X holds ex B be basis of x st B is compact;

        let x be Point of X, P be Subset of X such that

         A7: x in P and

         A8: P is open;

        consider B be basis of x such that

         A9: B is compact by A6;

        x in ( Int P) by A7, A8, TOPS_1: 23;

        then

        consider Q be Subset of X such that

         A10: Q in B and

         A11: x in ( Int Q) and

         A12: Q c= P by YELLOW13:def 1;

        take Q;

        thus x in ( Int Q) & Q c= P by A11, A12;

        thus thesis by A9, A10;

      end;

    end

    definition

      let X be non empty TopSpace;

      :: COMPACT1:def4

      attr X is locally-relatively-compact means for x be Point of X holds ex U be a_neighborhood of x st U is relatively-compact;

    end

    definition

      let X be non empty TopSpace;

      :: COMPACT1:def5

      attr X is locally-closed/compact means for x be Point of X holds ex U be a_neighborhood of x st U is closed compact;

    end

    definition

      let X be non empty TopSpace;

      :: COMPACT1:def6

      attr X is locally-compact means

      : Def6: for x be Point of X holds ex U be a_neighborhood of x st U is compact;

    end

    registration

      cluster liminally-compact -> locally-compact for non empty TopSpace;

      coherence

      proof

        let X be non empty TopSpace such that

         A1: X is liminally-compact;

        let x be Point of X;

        consider B be basis of x such that

         A2: B is compact by A1;

        set V = the a_neighborhood of x;

        consider Y be a_neighborhood of x such that

         A3: Y in B and Y c= V by YELLOW13:def 2;

        Y is compact by A2, A3;

        hence thesis;

      end;

    end

    registration

      cluster locally-compact -> liminally-compact for non empty regular TopSpace;

      coherence

      proof

        let X be non empty regular TopSpace such that

         A1: X is locally-compact;

        let x be Point of X;

        set B = { Q where Q be a_neighborhood of x : Q is compact & ex V,W be a_neighborhood of x st Q c= (V /\ W) };

        B c= ( bool ( [#] X))

        proof

          let A be object;

          assume A in B;

          then ex Q be a_neighborhood of x st A = Q & Q is compact & ex V,W be a_neighborhood of x st Q c= (V /\ W);

          hence thesis;

        end;

        then

        reconsider B as Subset-Family of X;

        

         A2: B is basis of x

        proof

          let V be a_neighborhood of x;

          

           A3: x in ( Int V) by CONNSP_2:def 1;

          consider W be a_neighborhood of x such that

           A4: W is compact by A1;

          x in ( Int W) by CONNSP_2:def 1;

          then x in (( Int V) /\ ( Int W)) by A3, XBOOLE_0:def 4;

          then x in ( Int (V /\ W)) by TOPS_1: 17;

          then

          consider Q be Subset of X such that

           A5: Q is closed and

           A6: Q c= (V /\ W) and

           A7: x in ( Int Q) by YELLOW_8: 27;

          reconsider Q as a_neighborhood of x by A7, CONNSP_2:def 1;

          take Q;

          (V /\ W) c= W by XBOOLE_1: 17;

          then Q is compact by A4, A5, A6, COMPTS_1: 9, XBOOLE_1: 1;

          hence Q in B by A6;

          (V /\ W) c= V by XBOOLE_1: 17;

          hence thesis by A6;

        end;

        B is compact

        proof

          let U be Subset of X;

          assume U in B;

          then ex Q be a_neighborhood of x st U = Q & Q is compact & ex V,W be a_neighborhood of x st Q c= (V /\ W);

          hence thesis;

        end;

        hence thesis by A2;

      end;

    end

    registration

      cluster locally-relatively-compact -> locally-closed/compact for non empty TopSpace;

      coherence

      proof

        let X be non empty TopSpace such that

         A1: X is locally-relatively-compact;

        let x be Point of X;

        consider U be a_neighborhood of x such that

         A2: U is relatively-compact by A1;

        

         A3: x in ( Int U) by CONNSP_2:def 1;

        ( Int U) c= ( Int ( Cl U)) by PRE_TOPC: 18, TOPS_1: 19;

        then ( Cl U) is a_neighborhood of x by A3, CONNSP_2:def 1;

        hence thesis by A2;

      end;

    end

    registration

      cluster locally-closed/compact -> locally-relatively-compact for non empty TopSpace;

      coherence

      proof

        let X be non empty TopSpace such that

         A1: X is locally-closed/compact;

        let x be Point of X;

        consider U be a_neighborhood of x such that

         A2: U is closed compact by A1;

        ( Cl U) = U by A2, PRE_TOPC: 22;

        then U is relatively-compact by A2;

        hence thesis;

      end;

    end

    registration

      cluster locally-relatively-compact -> locally-compact for non empty TopSpace;

      coherence

      proof

        let X be non empty TopSpace such that

         A1: X is locally-relatively-compact;

        let x be Point of X;

        consider Y be a_neighborhood of x such that

         A2: Y is relatively-compact by A1;

        

         A3: x in ( Int Y) by CONNSP_2:def 1;

        ( Int Y) c= ( Int ( Cl Y)) by PRE_TOPC: 18, TOPS_1: 19;

        then ( Cl Y) is a_neighborhood of x by A3, CONNSP_2:def 1;

        hence thesis by A2;

      end;

    end

    registration

      cluster locally-compact -> locally-relatively-compact for non empty Hausdorff TopSpace;

      coherence

      proof

        let X be non empty Hausdorff TopSpace such that

         A1: X is locally-compact;

        let x be Point of X;

        consider U be a_neighborhood of x such that

         A2: U is compact by A1;

        ( Cl U) = U by A2, PRE_TOPC: 22;

        then U is relatively-compact by A2;

        hence thesis;

      end;

    end

    registration

      cluster compact -> locally-compact for non empty TopSpace;

      coherence

      proof

        let X be non empty TopSpace;

        set Y = ( [#] X);

        assume

         A1: X is compact;

        let x be Point of X;

        ( Int Y) = Y by TOPS_1: 23;

        then Y is a_neighborhood of x by CONNSP_2:def 1;

        hence thesis by A1;

      end;

    end

    registration

      cluster discrete -> locally-compact for non empty TopSpace;

      coherence

      proof

        let X be non empty TopSpace such that

         A1: X is discrete;

        let x be Point of X;

        set Y = {x};

        Y is open by A1, TDLAT_3: 15;

        then ( Int Y) = Y by TOPS_1: 23;

        then x in ( Int Y) by TARSKI:def 1;

        then

        reconsider Y as a_neighborhood of x by CONNSP_2:def 1;

        Y is compact;

        hence thesis;

      end;

    end

    registration

      cluster discrete non empty for TopSpace;

      existence

      proof

        set X = the discrete non empty TopSpace;

        take X;

        thus thesis;

      end;

    end

    registration

      let X be locally-compact non empty TopSpace, C be closed non empty Subset of X;

      cluster (X | C) -> locally-compact;

      coherence

      proof

        let x be Point of (X | C);

        reconsider xx = x as Point of X by PRE_TOPC: 25;

        consider K be a_neighborhood of xx such that

         A1: K is compact by Def6;

        

         A2: ( [#] (X | C)) = C by PRE_TOPC: 8;

        then

        reconsider KC = (K /\ C) as Subset of (X | C) by XBOOLE_1: 17;

        reconsider KC as a_neighborhood of x by A2, TOPMETR: 5;

        take KC;

        

         A3: xx in ( Int K) by CONNSP_2:def 1;

        

         A4: ( [#] (X | K)) = K by PRE_TOPC: 8;

        then

        reconsider KK = (K /\ C) as Subset of (X | K) by XBOOLE_1: 17;

        

         A5: KK is closed by A4, PRE_TOPC: 13;

        

         A6: ( Int K) c= K by TOPS_1: 16;

        then

         A7: x in KC by A2, A3, XBOOLE_0:def 4;

        (X | K) is compact by A1, A6, A3, COMPTS_1: 3;

        then KK is compact by A5, COMPTS_1: 8;

        then ((X | K) | KK) is compact by A7, COMPTS_1: 3;

        then (X | (K /\ C)) is compact by PRE_TOPC: 7, XBOOLE_1: 17;

        then ((X | C) | KC) is compact by PRE_TOPC: 7, XBOOLE_1: 17;

        hence thesis by A7, COMPTS_1: 3;

      end;

    end

    registration

      let X be locally-compact non empty regular TopSpace, P be open non empty Subset of X;

      cluster (X | P) -> locally-compact;

      coherence

      proof

        let x be Point of (X | P);

        reconsider xx = x as Point of X by PRE_TOPC: 25;

        consider B be basis of xx such that

         A1: B is compact by Def3;

        

         A2: ( [#] (X | P)) = P by PRE_TOPC: 8;

        then xx in P;

        then xx in ( Int P) by TOPS_1: 23;

        then P is a_neighborhood of xx by CONNSP_2:def 1;

        then

        consider K be a_neighborhood of xx such that

         A3: K in B and

         A4: K c= P by YELLOW13:def 2;

        reconsider KK = K as Subset of (X | P) by A4, PRE_TOPC: 8;

        K is compact by A1, A3;

        then

         A5: KK is compact by A2, COMPTS_1: 2;

        

         A6: ( Int K) c= K by TOPS_1: 16;

        xx in ( Int K) by CONNSP_2:def 1;

        then

         A7: x in K by A6;

        KK = (K /\ P) by A4, XBOOLE_1: 28;

        then KK is a_neighborhood of x by A4, A7, TOPMETR: 5;

        hence thesis by A5;

      end;

    end

    theorem :: COMPACT1:1

    for X be Hausdorff non empty TopSpace, E be non empty Subset of X st (X | E) is dense locally-compact holds (X | E) is open

    proof

      let X be Hausdorff non empty TopSpace, E be non empty Subset of X such that

       A1: (X | E) is dense locally-compact;

      

       A2: ( [#] (X | E)) = E by PRE_TOPC: 8;

      ( Int E) = E

      proof

        thus ( Int E) c= E by TOPS_1: 16;

        let a be object;

        assume

         A3: a in E;

        then

        reconsider x = a as Point of X;

        reconsider xx = x as Point of (X | E) by A3, PRE_TOPC: 8;

        set UE = { G where G be Subset of X : G is open & G c= E };

        consider K be a_neighborhood of xx such that

         A4: K is compact by A1;

        reconsider KK = K as Subset of X by A2, XBOOLE_1: 1;

        

         A5: K c= ( [#] (X | E));

        ( Int K) in the topology of (X | E) by PRE_TOPC:def 2;

        then

        consider G be Subset of X such that

         A6: G in the topology of X and

         A7: ( Int K) = (G /\ E) by A2, PRE_TOPC:def 4;

        

         A8: G is open by A6;

        for P be Subset of (X | E) st P = KK holds P is compact by A4;

        then KK is compact by A5, COMPTS_1: 2;

        then

         A9: ( Cl (G /\ E)) c= KK by A7, TOPS_1: 5, TOPS_1: 16;

        E is dense by A1, A2, TEX_3:def 1;

        then

         A10: ( Cl (G /\ E)) = ( Cl G) by A8, TOPS_1: 46;

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

        then G c= K by A10, A9;

        then G c= E by A2, XBOOLE_1: 1;

        then

         A11: G in UE by A8;

        

         A12: xx in ( Int K) by CONNSP_2:def 1;

        ( Int K) c= G by A7, XBOOLE_1: 17;

        then a in ( union UE) by A12, A11, TARSKI:def 4;

        hence thesis by TEX_4: 3;

      end;

      hence thesis by A2, TSEP_1: 16;

    end;

    theorem :: COMPACT1:2

    

     Th2: for X,Y be TopSpace, A be Subset of X st ( [#] X) c= ( [#] Y) holds (( incl (X,Y)) .: A) = A

    proof

      let X,Y be TopSpace, A be Subset of X;

      assume ( [#] X) c= ( [#] Y);

      

      hence (( incl (X,Y)) .: A) = (( id ( [#] X)) .: A) by YELLOW_9:def 1

      .= A by FUNCT_1: 92;

    end;

    definition

      let X,Y be TopSpace, f be Function of X, Y;

      :: COMPACT1:def7

      attr f is embedding means ex h be Function of X, (Y | ( rng f)) st h = f & h is being_homeomorphism;

    end

    theorem :: COMPACT1:3

    

     Th3: for X,Y be TopSpace st ( [#] X) c= ( [#] Y) & ex Xy be Subset of Y st Xy = ( [#] X) & the topology of (Y | Xy) = the topology of X holds ( incl (X,Y)) is embedding

    proof

      let X,Y be TopSpace such that

       A1: ( [#] X) c= ( [#] Y);

      

       A2: ( incl (X,Y)) = ( id X) by A1, YELLOW_9:def 1;

      set YY = (Y | ( rng ( incl (X,Y))));

      

       A3: ( [#] YY) = ( rng ( incl (X,Y))) by PRE_TOPC:def 5;

      

       A4: ( [#] Y) = {} implies ( [#] X) = {} by A1;

      then

      reconsider h = ( incl (X,Y)) as Function of X, YY by A3, FUNCT_2: 6;

      set f = ( id X);

      given Xy be Subset of Y such that

       A5: Xy = ( [#] X) and

       A6: the topology of (Y | Xy) = the topology of X;

      

       A7: for P be Subset of X st P is open holds ((h " ) " P) is open

      proof

        let P be Subset of X;

        reconsider Q = P as Subset of YY by A2, A3;

        assume P is open;

        then

         A8: P in the topology of X;

        ((h " ) " P) = (h .: Q) by A2, A3, TOPS_2: 54

        .= Q by A2, FUNCT_1: 92;

        hence ((h " ) " P) in the topology of YY by A5, A6, A2, A8;

      end;

      

       A9: ( [#] X) = {} implies ( [#] X) = {} ;

      

       A10: for P be Subset of YY st P is open holds (h " P) is open

      proof

        let P be Subset of YY;

        reconsider Q = P as Subset of X by A2, A3;

        assume P is open;

        then P in the topology of YY;

        then Q in the topology of X by A5, A6, A2;

        then Q is open;

        then (f " Q) is open by A9, TOPS_2: 43;

        then (f " Q) in the topology of X;

        hence (h " P) in the topology of X by A1, YELLOW_9:def 1;

      end;

      take h;

      thus h = ( incl (X,Y));

      thus ( dom h) = ( [#] X) & ( rng h) = ( [#] YY) by A4, FUNCT_2:def 1, PRE_TOPC:def 5;

      thus h is one-to-one by A2;

      ( [#] YY) = {} implies ( [#] X) = {} by A2, A3;

      hence h is continuous by A10, TOPS_2: 43;

      ( [#] X) = {} implies ( [#] YY) = {} ;

      hence thesis by A7, TOPS_2: 43;

    end;

    definition

      let X be TopSpace, Y be TopSpace, h be Function of X, Y;

      :: COMPACT1:def8

      attr h is compactification means h is embedding & Y is compact & (h .: ( [#] X)) is dense;

    end

    registration

      let X be TopSpace, Y be TopSpace;

      cluster compactification -> embedding for Function of X, Y;

      coherence ;

    end

    definition

      let X be TopStruct;

      :: COMPACT1:def9

      func One-Point_Compactification (X) -> strict TopStruct means

      : Def9: the carrier of it = ( succ ( [#] X)) & the topology of it = (the topology of X \/ { (U \/ {( [#] X)}) where U be Subset of X : U is open & (U ` ) is compact });

      existence

      proof

        set T = ( succ ( [#] X)), D = { (U \/ {( [#] X)}) where U be Subset of X : U is open & (U ` ) is compact }, O = (the topology of X \/ D);

        O c= ( bool T)

        proof

          let a be object;

          reconsider aa = a as set by TARSKI: 1;

           A1:

          now

            assume a in D;

            then

            consider U be Subset of X such that

             A2: a = (U \/ {( [#] X)}) and U is open and (U ` ) is compact;

            thus aa c= T

            proof

              let A be object;

              assume A in aa;

              then A in U or A in {( [#] X)} by A2, XBOOLE_0:def 3;

              hence thesis by XBOOLE_0:def 3;

            end;

          end;

          assume a in O;

          then a in the topology of X or a in D by XBOOLE_0:def 3;

          then a is Subset of T by A1, XBOOLE_1: 10;

          hence thesis;

        end;

        then

        reconsider O as Subset-Family of T;

        set Y = TopStruct (# T, O #);

        Y is non empty;

        hence thesis;

      end;

      uniqueness ;

    end

    registration

      let X be TopStruct;

      cluster ( One-Point_Compactification X) -> non empty;

      coherence

      proof

        the carrier of ( One-Point_Compactification X) = ( succ ( [#] X)) by Def9;

        hence thesis;

      end;

    end

    theorem :: COMPACT1:4

    

     Th4: for X be TopStruct holds ( [#] X) c= ( [#] ( One-Point_Compactification X))

    proof

      let X be TopStruct;

      ( [#] ( One-Point_Compactification X)) = ( succ ( [#] X)) by Def9;

      hence thesis by XBOOLE_1: 7;

    end;

    registration

      let X be TopSpace;

      cluster ( One-Point_Compactification X) -> TopSpace-like;

      coherence

      proof

        set Y = ( One-Point_Compactification X);

        set T = ( succ ( [#] X)), D = { (U \/ {( [#] X)}) where U be Subset of X : U is open & (U ` ) is compact };

        

         A1: not ( [#] X) in ( [#] X);

        

         A2: the topology of ( One-Point_Compactification X) = (the topology of X \/ D) by Def9;

        

         A3: ( [#] ( One-Point_Compactification X)) = T by Def9;

        Y is TopSpace-like

        proof

          (( [#] X) ` ) = ((( {} X) ` ) ` )

          .= ( {} X);

          then T in D;

          hence the carrier of Y in the topology of Y by A3, A2, XBOOLE_0:def 3;

          hereby

            let a be Subset-Family of Y;

            

             A4: not ( [#] X) in ( [#] X);

            set ua = { U where U be Subset of X : U is open & (U in a or (U \/ {( [#] X)}) in a) };

            

             A5: ua c= the topology of X

            proof

              let x be object;

              assume x in ua;

              then ex U be Subset of X st x = U & U is open & (U in a or (U \/ {( [#] X)}) in a);

              hence thesis;

            end;

            then

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

            ( union ua) in the topology of X by A5, PRE_TOPC:def 1;

            then

             A6: ( union ua) is open;

            assume

             A7: a c= the topology of Y;

            

             A8: ( union ua) = (( union a) \ {( [#] X)})

            proof

              thus ( union ua) c= (( union a) \ {( [#] X)})

              proof

                let x be object;

                assume x in ( union ua);

                then

                consider A be set such that

                 A9: x in A and

                 A10: A in ua by TARSKI:def 4;

                consider U be Subset of X such that

                 A11: A = U and U is open and

                 A12: U in a or (U \/ {( [#] X)}) in a by A10;

                 A13:

                now

                  per cases by A12;

                    suppose U in a;

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

                  end;

                    suppose

                     A14: (U \/ {( [#] X)}) in a;

                    x in (U \/ {( [#] X)}) by A9, A11, XBOOLE_0:def 3;

                    hence x in ( union a) by A14, TARSKI:def 4;

                  end;

                end;

                now

                  assume x in {( [#] X)};

                  then

                   A15: x = ( [#] X) by TARSKI:def 1;

                  

                   A: x in ( [#] X) by A9, A11;

                  reconsider xx = x as set by TARSKI: 1;

                   not xx in xx;

                  hence contradiction by A, A15;

                end;

                hence thesis by A13, XBOOLE_0:def 5;

              end;

              let x be object;

              assume

               A16: x in (( union a) \ {( [#] X)});

              then x in ( union a) by XBOOLE_0:def 5;

              then

              consider A be set such that

               A17: x in A and

               A18: A in a by TARSKI:def 4;

              per cases by A2, A7, A18, XBOOLE_0:def 3;

                suppose

                 A19: A in the topology of X;

                then

                reconsider U = A as Subset of X;

                U is open by A19;

                then U in ua by A18;

                hence thesis by A17, TARSKI:def 4;

              end;

                suppose A in D;

                then

                consider U be Subset of X such that

                 A20: A = (U \/ {( [#] X)}) and

                 A21: U is open and (U ` ) is compact;

                

                 A22: U in ua by A18, A20, A21;

                 not x in {( [#] X)} by A16, XBOOLE_0:def 5;

                then x in U by A17, A20, XBOOLE_0:def 3;

                hence thesis by A22, TARSKI:def 4;

              end;

            end;

            per cases ;

              suppose

               A23: ( [#] X) in ( union a);

              then

              consider A be set such that

               A24: ( [#] X) in A and

               A25: A in a by TARSKI:def 4;

              A in the topology of X or A in D by A2, A7, A25, XBOOLE_0:def 3;

              then

              consider U be Subset of X such that

               A26: A = (U \/ {( [#] X)}) and U is open and

               A27: (U ` ) is compact by A4, A24;

               A28:

              now

                assume ( [#] X) in U;

                then ( [#] X) in ( [#] X);

                hence contradiction;

              end;

              (A \ {( [#] X)}) = (U \ {( [#] X)}) by A26, XBOOLE_1: 40

              .= U by A28, ZFMISC_1: 57;

              then U c= ( union ua) by A8, A25, XBOOLE_1: 33, ZFMISC_1: 74;

              then

               A29: (( union ua) ` ) is compact by A6, A27, COMPTS_1: 9, XBOOLE_1: 34;

              (( union ua) \/ {( [#] X)}) = (( union a) \/ {( [#] X)}) by A8, XBOOLE_1: 39

              .= ( union a) by A23, ZFMISC_1: 40;

              then ( union a) in D by A6, A29;

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

            end;

              suppose

               A30: not ( [#] X) in ( union a);

              

               A31: a c= the topology of X

              proof

                let A be object;

                reconsider AA = A as set by TARSKI: 1;

                assume

                 A32: A in a;

                assume not A in the topology of X;

                then A in D by A2, A7, A32, XBOOLE_0:def 3;

                then

                 A33: ex U be Subset of X st A = (U \/ {( [#] X)}) & U is open & (U ` ) is compact;

                ( [#] X) in {( [#] X)} by TARSKI:def 1;

                then ( [#] X) in AA by A33, XBOOLE_0:def 3;

                hence contradiction by A30, A32, TARSKI:def 4;

              end;

              then a is Subset-Family of ( [#] X) by XBOOLE_1: 1;

              then ( union a) in the topology of X by A31, PRE_TOPC:def 1;

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

            end;

          end;

          let a,b be Subset of Y;

          assume

           A34: a in the topology of Y;

          assume

           A35: b in the topology of Y;

          per cases by A2, A34, A35, XBOOLE_0:def 3;

            suppose a in the topology of X & b in the topology of X;

            then (a /\ b) in the topology of X by PRE_TOPC:def 1;

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

          end;

            suppose that

             A36: a in the topology of X and

             A37: b in D;

            reconsider a9 = a as Subset of X by A36;

             not ( [#] X) in a9 by A1;

            then {( [#] X)} misses a9 by ZFMISC_1: 50;

            then (a9 /\ {( [#] X)}) = ( {} X);

            then

            reconsider aX = (a9 /\ {( [#] X)}) as open Subset of X;

            consider U be Subset of X such that

             A38: b = (U \/ {( [#] X)}) and

             A39: U is open and (U ` ) is compact by A37;

            a9 is open by A36;

            then

            reconsider aXU = (a9 /\ U) as open Subset of X by A39;

            (a /\ b) = (aXU \/ aX) by A38, XBOOLE_1: 23;

            then (a /\ b) in the topology of X by PRE_TOPC:def 2;

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

          end;

            suppose that

             A40: b in the topology of X and

             A41: a in D;

            reconsider b9 = b as Subset of X by A40;

             not ( [#] X) in b9 by A1;

            then {( [#] X)} misses b9 by ZFMISC_1: 50;

            then (b9 /\ {( [#] X)}) = ( {} X);

            then

            reconsider bX = (b9 /\ {( [#] X)}) as open Subset of X;

            consider U be Subset of X such that

             A42: a = (U \/ {( [#] X)}) and

             A43: U is open and (U ` ) is compact by A41;

            b9 is open by A40;

            then

            reconsider bXUa = (b9 /\ U) as open Subset of X by A43;

            (a /\ b) = (bXUa \/ bX) by A42, XBOOLE_1: 23;

            then (a /\ b) in the topology of X by PRE_TOPC:def 2;

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

          end;

            suppose that

             A44: a in D and

             A45: b in D;

            consider Ua be Subset of X such that

             A46: a = (Ua \/ {( [#] X)}) and

             A47: Ua is open and

             A48: (Ua ` ) is compact by A44;

            consider Ub be Subset of X such that

             A49: b = (Ub \/ {( [#] X)}) and

             A50: Ub is open and

             A51: (Ub ` ) is compact by A45;

            ((Ua ` ) \/ (Ub ` )) is compact by A48, A51, COMPTS_1: 10;

            then

             A52: ((Ua /\ Ub) ` ) is compact by XBOOLE_1: 54;

            (a /\ b) = ((Ua /\ Ub) \/ {( [#] X)}) by A46, A49, XBOOLE_1: 24;

            then (a /\ b) in D by A47, A50, A52;

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

          end;

        end;

        hence thesis;

      end;

    end

    theorem :: COMPACT1:5

    

     Th5: for X be TopStruct holds X is SubSpace of ( One-Point_Compactification X)

    proof

      let X be TopStruct;

      set D = { (U \/ {( [#] X)}) where U be Subset of X : U is open & (U ` ) is compact };

      thus

       A1: ( [#] X) c= ( [#] ( One-Point_Compactification X)) by Th4;

      let P be Subset of X;

      

       A2: the topology of ( One-Point_Compactification X) = (the topology of X \/ D) by Def9;

      hereby

        reconsider Q = P as Subset of ( One-Point_Compactification X) by A1, XBOOLE_1: 1;

        assume

         A3: P in the topology of X;

        take Q;

        thus Q in the topology of ( One-Point_Compactification X) by A2, A3, XBOOLE_0:def 3;

        thus P = (Q /\ ( [#] X)) by XBOOLE_1: 28;

      end;

      given Q be Subset of ( One-Point_Compactification X) such that

       A4: Q in the topology of ( One-Point_Compactification X) and

       A5: P = (Q /\ ( [#] X));

      per cases by A2, A4, XBOOLE_0:def 3;

        suppose Q in the topology of X;

        hence thesis by A5, XBOOLE_1: 28;

      end;

        suppose Q in D;

        then

        consider U be Subset of X such that

         A6: Q = (U \/ {( [#] X)}) and

         A7: U is open and (U ` ) is compact;

         not ( [#] X) in ( [#] X);

        then {( [#] X)} misses ( [#] X) by ZFMISC_1: 50;

        then ( {( [#] X)} /\ ( [#] X)) = {} ;

        

        then P = ((U /\ ( [#] X)) \/ {} ) by A5, A6, XBOOLE_1: 23

        .= U by XBOOLE_1: 28;

        hence thesis by A7;

      end;

    end;

    registration

      let X be TopSpace;

      cluster ( One-Point_Compactification X) -> compact;

      coherence

      proof

        set D = { (U \/ {( [#] X)}) where U be Subset of X : U is open & (U ` ) is compact };

        let F be Subset-Family of ( One-Point_Compactification X) such that

         A1: F is Cover of ( One-Point_Compactification X) and

         A2: F is open;

        

         A3: ( [#] ( One-Point_Compactification X)) c= ( union F) by A1, SETFAM_1:def 11;

        set Fx = { U where U be Subset of X : U is open & (U in F & not (U \/ {( [#] X)}) in F or (U \/ {( [#] X)}) in F) };

        Fx c= the topology of X

        proof

          let x be object;

          assume x in Fx;

          then ex U be Subset of X st x = U & U is open & (U in F & not (U \/ {( [#] X)}) in F or (U \/ {( [#] X)}) in F);

          hence thesis;

        end;

        then

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

        

         A4: Fx is open

        proof

          let P be Subset of X;

          assume P in Fx;

          then ex U be Subset of X st P = U & U is open & (U in F & not (U \/ {( [#] X)}) in F or (U \/ {( [#] X)}) in F);

          hence thesis;

        end;

        ( [#] X) in {( [#] X)} by TARSKI:def 1;

        then ( [#] X) in ( succ ( [#] X)) by XBOOLE_0:def 3;

        then ( [#] X) in ( [#] ( One-Point_Compactification X)) by Def9;

        then

        consider A be set such that

         A5: ( [#] X) in A and

         A6: A in F by A3, TARSKI:def 4;

        reconsider A as Subset of ( One-Point_Compactification X) by A6;

        A is open by A2, A6;

        then A in the topology of ( One-Point_Compactification X);

        then

         A7: A in (the topology of X \/ D) by Def9;

         not ( [#] X) in ( [#] X);

        then not A in the topology of X by A5;

        then A in D by A7, XBOOLE_0:def 3;

        then

        consider U be Subset of X such that

         A8: A = (U \/ {( [#] X)}) and U is open and

         A9: (U ` ) is compact;

        Fx is Cover of X

        proof

          let x be object;

          assume

           A10: x in the carrier of X;

          then x in ( succ ( [#] X)) by XBOOLE_0:def 3;

          then x in ( [#] ( One-Point_Compactification X)) by Def9;

          then

          consider B be set such that

           A11: x in B and

           A12: B in F by A3, TARSKI:def 4;

          reconsider B as Subset of ( One-Point_Compactification X) by A12;

          B is open by A2, A12;

          then B in the topology of ( One-Point_Compactification X);

          then

           A13: B in (the topology of X \/ D) by Def9;

          per cases by A13, XBOOLE_0:def 3;

            suppose

             A14: B in the topology of X;

            then

            reconsider Bx = B as Subset of X;

            

             A15: Bx in F & not (Bx \/ {( [#] X)}) in F or (Bx \/ {( [#] X)}) in F by A12;

            Bx is open by A14;

            then Bx in Fx by A15;

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

          end;

            suppose B in D;

            then

            consider Bx be Subset of X such that

             A16: B = (Bx \/ {( [#] X)}) and

             A17: Bx is open and (Bx ` ) is compact;

            

             A18: Bx in Fx by A12, A16, A17;

            now

              assume x in {( [#] X)};

              then

               A: x = ( [#] X) by TARSKI:def 1;

              reconsider xx = x as set by TARSKI: 1;

               not xx in xx;

              hence contradiction by A, A10;

            end;

            then x in Bx by A11, A16, XBOOLE_0:def 3;

            hence x in ( union Fx) by A18, TARSKI:def 4;

          end;

        end;

        then ( [#] X) = ( union Fx) by SETFAM_1: 45;

        then Fx is Cover of (U ` ) by SETFAM_1:def 11;

        then

        consider Gx be Subset-Family of X such that

         A19: Gx c= Fx and

         A20: Gx is Cover of (U ` ) and

         A21: Gx is finite by A9, A4;

        set GX = { W where W be Subset of ( One-Point_Compactification X) : W in F & ex V be Subset of X st V in Gx & (V in F & not (V \/ {( [#] X)}) in F & W = V or (V \/ {( [#] X)}) in F & W = (V \/ {( [#] X)})) };

        

         A22: GX c= the topology of ( One-Point_Compactification X)

        proof

          let x be object;

          assume x in GX;

          then

          consider W be Subset of ( One-Point_Compactification X) such that

           A23: x = W and

           A24: W in F and ex V be Subset of X st V in Gx & (V in F & not (V \/ {( [#] X)}) in F & W = V or (V \/ {( [#] X)}) in F & W = (V \/ {( [#] X)}));

          W is open by A2, A24;

          hence thesis by A23;

        end;

        defpred P[ object, object] means ex D1 be set st D1 = $1 & ($1 in Gx & ((D1 \/ {( [#] X)}) in F implies $2 = (D1 \/ {( [#] X)})) & ( not (D1 \/ {( [#] X)}) in F implies $2 = $1));

        

         A25: for x be object st x in Gx holds ex y be object st y in GX & P[x, y]

        proof

          let x be object;

          assume

           A26: x in Gx;

          then x in Fx by A19;

          then

          consider U be Subset of X such that

           A27: x = U and U is open and

           A28: U in F & not (U \/ {( [#] X)}) in F or (U \/ {( [#] X)}) in F;

          per cases ;

            suppose

             A29: not (U \/ {( [#] X)}) in F;

            then

            reconsider y = U as Subset of ( One-Point_Compactification X) by A28;

            reconsider y as object;

            take y;

            thus y in GX by A26, A27, A28, A29;

            thus thesis by A26, A27, A29;

          end;

            suppose

             A30: (U \/ {( [#] X)}) in F;

            then

            reconsider y = (U \/ {( [#] X)}) as Subset of ( One-Point_Compactification X);

            take y;

            thus y in GX by A26, A27, A30;

            thus thesis by A26, A27, A30;

          end;

        end;

        consider f be Function such that

         A31: ( dom f) = Gx and ( rng f) c= GX and

         A32: for x be object st x in Gx holds P[x, (f . x)] from FUNCT_1:sch 6( A25);

        

         A33: GX c= ( rng f)

        proof

          let y be object;

          assume y in GX;

          then

          consider W be Subset of ( One-Point_Compactification X) such that

           A34: y = W and W in F and

           A35: ex V be Subset of X st V in Gx & (V in F & not (V \/ {( [#] X)}) in F & W = V or (V \/ {( [#] X)}) in F & W = (V \/ {( [#] X)}));

          consider V be Subset of X such that

           A36: V in Gx and

           A37: V in F & not (V \/ {( [#] X)}) in F & W = V or (V \/ {( [#] X)}) in F & W = (V \/ {( [#] X)}) by A35;

          

           A38: (f . V) in ( rng f) by A31, A36, FUNCT_1: 3;

           P[V, (f . V)] by A32, A36;

          hence thesis by A34, A37, A38;

        end;

        ( rng f) is finite by A21, A31, FINSET_1: 8;

        then

        reconsider GX as finite Subset-Family of ( One-Point_Compactification X) by A33, A22, XBOOLE_1: 1;

        take G = (GX \/ {A});

        

         A39: GX c= F

        proof

          let P be object;

          assume P in GX;

          then ex W be Subset of ( One-Point_Compactification X) st P = W & W in F & ex V be Subset of X st V in Gx & (V in F & not (V \/ {( [#] X)}) in F & W = V or (V \/ {( [#] X)}) in F & W = (V \/ {( [#] X)}));

          hence thesis;

        end;

         {A} c= F by A6, ZFMISC_1: 31;

        hence G c= F by A39, XBOOLE_1: 8;

        ( union G) = ( [#] ( One-Point_Compactification X))

        proof

          thus ( union G) c= ( [#] ( One-Point_Compactification X));

          let P be object;

          assume P in ( [#] ( One-Point_Compactification X));

          then

           A40: P in ( succ ( [#] X)) by Def9;

          per cases by A40, XBOOLE_0:def 3;

            suppose P in ( [#] X);

            then P in ((U ` ) \/ U) by PRE_TOPC: 2;

            then

             A41: P in (U ` ) or P in U by XBOOLE_0:def 3;

            

             A42: ( union Gx) c= ( union GX)

            proof

              let z be object;

              assume z in ( union Gx);

              then

              consider S be set such that

               A43: z in S and

               A44: S in Gx by TARSKI:def 4;

              S in Fx by A19, A44;

              then

              consider Z be Subset of X such that

               A45: S = Z and Z is open and

               A46: Z in F & not (Z \/ {( [#] X)}) in F or (Z \/ {( [#] X)}) in F;

              per cases by A46;

                suppose Z in F & not (Z \/ {( [#] X)}) in F;

                then Z in GX by A44, A45;

                hence thesis by A43, A45, TARSKI:def 4;

              end;

                suppose

                 A47: (Z \/ {( [#] X)}) in F;

                

                 A48: z in (Z \/ {( [#] X)}) by A43, A45, XBOOLE_0:def 3;

                (Z \/ {( [#] X)}) in GX by A44, A45, A47;

                hence thesis by A48, TARSKI:def 4;

              end;

            end;

            (U ` ) c= ( union Gx) by A20, SETFAM_1:def 11;

            then P in ( union Gx) or P in U by A41;

            then P in ( union GX) or P in A by A8, A42, XBOOLE_0:def 3;

            then P in ( union GX) or P in ( union {A}) by ZFMISC_1: 25;

            then P in (( union GX) \/ ( union {A})) by XBOOLE_0:def 3;

            hence thesis by ZFMISC_1: 78;

          end;

            suppose

             A49: P in {( [#] X)};

            A in {A} by TARSKI:def 1;

            then

             A50: A in G by XBOOLE_0:def 3;

            P = ( [#] X) by A49, TARSKI:def 1;

            hence thesis by A5, A50, TARSKI:def 4;

          end;

        end;

        hence G is Cover of ( One-Point_Compactification X) by SETFAM_1:def 11;

        thus thesis;

      end;

    end

    theorem :: COMPACT1:6

    for X be non empty TopSpace holds X is Hausdorff locally-compact iff ( One-Point_Compactification X) is Hausdorff

    proof

      let X be non empty TopSpace;

      set D = { (U \/ {( [#] X)}) where U be Subset of X : U is open & (U ` ) is compact };

      

       A1: not ( [#] X) in ( [#] X);

      

       A2: ( [#] ( One-Point_Compactification X)) = ( succ ( [#] X)) by Def9;

      ( [#] X) in {( [#] X)} by TARSKI:def 1;

      then

      reconsider q = ( [#] X) as Point of ( One-Point_Compactification X) by A2, XBOOLE_0:def 3;

      

       A3: the topology of ( One-Point_Compactification X) = (the topology of X \/ D) by Def9;

      

       A4: ( [#] X) c= ( [#] ( One-Point_Compactification X)) by Th4;

      thus X is Hausdorff locally-compact implies ( One-Point_Compactification X) is Hausdorff

      proof

        assume that

         A5: X is Hausdorff and

         A6: X is locally-compact;

        let p,q be Point of ( One-Point_Compactification X) such that

         A7: p <> q;

        per cases by A2, XBOOLE_0:def 3;

          suppose p in ( [#] X) & q in ( [#] X);

          then

          consider W,V be Subset of X such that

           A8: W is open and

           A9: V is open and

           A10: p in W and

           A11: q in V and

           A12: W misses V by A5, A7;

          reconsider W, V as Subset of ( One-Point_Compactification X) by A4, XBOOLE_1: 1;

          V in the topology of X by A9;

          then

           A13: V in the topology of ( One-Point_Compactification X) by A3, XBOOLE_0:def 3;

          take W, V;

          W in the topology of X by A8;

          then W in the topology of ( One-Point_Compactification X) by A3, XBOOLE_0:def 3;

          hence W is open & V is open by A13;

          thus thesis by A10, A11, A12;

        end;

          suppose that

           A14: p in ( [#] X) and

           A15: q in {( [#] X)};

          reconsider px = p as Point of X by A14;

          consider P be a_neighborhood of px such that

           A16: P is compact by A6;

          ( [#] X) c= ( [#] ( One-Point_Compactification X)) by A2, XBOOLE_1: 7;

          then

          reconsider W = ( Int P) as Subset of ( One-Point_Compactification X) by XBOOLE_1: 1;

          ((P ` ) ` ) = P;

          then ((P ` ) \/ {( [#] X)}) in D by A5, A16;

          then

           A17: ((P ` ) \/ {( [#] X)}) in the topology of ( One-Point_Compactification X) by A3, XBOOLE_0:def 3;

          then

          reconsider V = ((P ` ) \/ {( [#] X)}) as Subset of ( One-Point_Compactification X);

          take W, V;

          W in the topology of X by PRE_TOPC:def 2;

          then W in the topology of ( One-Point_Compactification X) by A3, XBOOLE_0:def 3;

          hence W is open;

          thus V is open by A17;

          thus p in W by CONNSP_2:def 1;

          thus q in V by A15, XBOOLE_0:def 3;

           not ( [#] X) in ( [#] X);

          then not ( [#] X) in ( Int P);

          then

           A18: ( Int P) misses {( [#] X)} by ZFMISC_1: 50;

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

          then ( Int P) misses (P ` ) by SUBSET_1: 24;

          hence thesis by A18, XBOOLE_1: 70;

        end;

          suppose that

           A19: q in ( [#] X) and

           A20: p in {( [#] X)};

          reconsider qx = q as Point of X by A19;

          consider Q be a_neighborhood of qx such that

           A21: Q is compact by A6;

          ( [#] X) c= ( [#] ( One-Point_Compactification X)) by Th4;

          then

          reconsider W = ( Int Q) as Subset of ( One-Point_Compactification X) by XBOOLE_1: 1;

          ((Q ` ) ` ) = Q;

          then ((Q ` ) \/ {( [#] X)}) in D by A5, A21;

          then

           A22: ((Q ` ) \/ {( [#] X)}) in the topology of ( One-Point_Compactification X) by A3, XBOOLE_0:def 3;

          then

          reconsider V = ((Q ` ) \/ {( [#] X)}) as Subset of ( One-Point_Compactification X);

          take V, W;

          thus V is open by A22;

          W in the topology of X by PRE_TOPC:def 2;

          then W in the topology of ( One-Point_Compactification X) by A3, XBOOLE_0:def 3;

          hence W is open;

          thus p in V by A20, XBOOLE_0:def 3;

          thus q in W by CONNSP_2:def 1;

           not ( [#] X) in ( [#] X);

          then not ( [#] X) in ( Int Q);

          then

           A23: ( Int Q) misses {( [#] X)} by ZFMISC_1: 50;

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

          then ( Int Q) misses (Q ` ) by SUBSET_1: 24;

          hence thesis by A23, XBOOLE_1: 70;

        end;

          suppose

           A24: p in {( [#] X)} & q in {( [#] X)};

          then p = ( [#] X) by TARSKI:def 1;

          hence thesis by A7, A24, TARSKI:def 1;

        end;

      end;

      

       A25: X is SubSpace of ( One-Point_Compactification X) by Th5;

      assume

       A26: ( One-Point_Compactification X) is Hausdorff;

      hence X is Hausdorff by A25;

      let x be Point of X;

      reconsider p = x as Point of ( One-Point_Compactification X) by A4;

       not ( [#] X) in ( [#] X);

      then p <> q;

      then

      consider V,U be Subset of ( One-Point_Compactification X) such that

       A27: V is open and

       A28: U is open and

       A29: p in V and

       A30: q in U and

       A31: V misses U by A26;

       A32:

      now

        assume U in the topology of X;

        then q in ( [#] X) by A30;

        hence contradiction;

      end;

      U in the topology of ( One-Point_Compactification X) by A28;

      then U in D by A3, A32, XBOOLE_0:def 3;

      then

      consider W be Subset of X such that

       A33: U = (W \/ {( [#] X)}) and W is open and

       A34: (W ` ) is compact;

      

       A35: (( [#] X) \ U) = ((( [#] X) \ W) /\ (( [#] X) \ {( [#] X)})) by A33, XBOOLE_1: 53

      .= ((( [#] X) \ W) /\ ( [#] X)) by A1, ZFMISC_1: 57

      .= (( [#] X) \ W) by XBOOLE_1: 28;

      

       A36: ( [#] X) in {( [#] X)} by TARSKI:def 1;

      then

       A37: ( [#] X) in U by A33, XBOOLE_0:def 3;

      

       A38: (( [#] ( One-Point_Compactification X)) \ U) = ((( [#] X) \ U) \/ ( {( [#] X)} \ U)) by A2, XBOOLE_1: 42

      .= ((( [#] X) \ W) \/ {} ) by A37, A35, ZFMISC_1: 60

      .= (W ` );

      

       A39: V c= (U ` ) by A31, SUBSET_1: 23;

      then

       A40: V c= ( [#] X) by A38, XBOOLE_1: 1;

       A41:

      now

        assume V in D;

        then ex S be Subset of X st V = (S \/ {( [#] X)}) & S is open & (S ` ) is compact;

        then ( [#] X) in V by A36, XBOOLE_0:def 3;

        then ( [#] X) in ( [#] X) by A40;

        hence contradiction;

      end;

      V in the topology of ( One-Point_Compactification X) by A27;

      then V in the topology of X by A3, A41, XBOOLE_0:def 3;

      then

      reconsider Vx = V as open Subset of X by PRE_TOPC:def 2;

      set K = ( Cl Vx);

      

       A42: ( Int Vx) c= ( Int K) by PRE_TOPC: 18, TOPS_1: 19;

      x in ( Int Vx) by A29, TOPS_1: 23;

      then

      reconsider K as a_neighborhood of x by A42, CONNSP_2:def 1;

      take K;

      ((U ` ) /\ ( [#] X)) = (W ` ) by A38, XBOOLE_1: 28;

      then (W ` ) is closed by A25, A28, PRE_TOPC: 13;

      hence thesis by A34, A39, A38, COMPTS_1: 9, TOPS_1: 5;

    end;

    theorem :: COMPACT1:7

    

     Th7: for X be non empty TopSpace holds X is non compact iff ex X9 be Subset of ( One-Point_Compactification X) st X9 = ( [#] X) & X9 is dense

    proof

      let X be non empty TopSpace;

      set D = { (U \/ {( [#] X)}) where U be Subset of X : U is open & (U ` ) is compact };

      

       A1: not ( [#] X) in ( [#] X);

      

       A2: ( [#] ( One-Point_Compactification X)) = ( succ ( [#] X)) by Def9;

      

       A3: ( [#] X) in {( [#] X)} by TARSKI:def 1;

      then

       A4: ( [#] X) in ( [#] ( One-Point_Compactification X)) by A2, XBOOLE_0:def 3;

      

       A5: the topology of ( One-Point_Compactification X) = (the topology of X \/ D) by Def9;

      thus X is non compact implies ex X9 be Subset of ( One-Point_Compactification X) st X9 = ( [#] X) & X9 is dense

      proof

        assume X is non compact;

        then

         A6: ( [#] X) is non compact;

        ( [#] X) c= ( [#] ( One-Point_Compactification X)) by Th4;

        then

        reconsider X9 = ( [#] X) as Subset of ( One-Point_Compactification X);

        take X9;

        thus X9 = ( [#] X);

        thus ( Cl X9) c= ( [#] ( One-Point_Compactification X));

        

         A7: ( [#] X) c= ( Cl X9) by PRE_TOPC: 18;

         A8:

        now

          reconsider Xe = ( [#] X) as Element of ( One-Point_Compactification X) by A3, A2, XBOOLE_0:def 3;

          assume

           A9: not ( [#] X) in ( Cl X9);

          reconsider XX = {Xe} as Subset of ( One-Point_Compactification X);

           A10:

          now

            assume XX in the topology of X;

            then ( [#] X) in ( [#] X) by A3;

            hence contradiction;

          end;

          (( [#] ( One-Point_Compactification X)) \ ( Cl X9)) = ((( [#] X) \ ( Cl X9)) \/ ( {( [#] X)} \ ( Cl X9))) by A2, XBOOLE_1: 42

          .= ( {} \/ ( {( [#] X)} \ ( Cl X9))) by A7, XBOOLE_1: 37

          .= XX by A9, ZFMISC_1: 59;

          then XX is open by PRE_TOPC:def 3;

          then XX in the topology of ( One-Point_Compactification X);

          then XX in D by A5, A10, XBOOLE_0:def 3;

          then

          consider U be Subset of X such that

           A11: XX = (U \/ {( [#] X)}) and U is open and

           A12: (U ` ) is compact;

          now

            assume U = XX;

            then ( [#] X) in ( [#] X) by A3;

            hence contradiction;

          end;

          then U = ( {} X) by A11, ZFMISC_1: 37;

          hence contradiction by A6, A12;

        end;

        ( [#] ( One-Point_Compactification X)) c= (( Cl X9) \/ {( [#] X)}) by A2, PRE_TOPC: 18, XBOOLE_1: 9;

        hence thesis by A8, ZFMISC_1: 40;

      end;

      given X9 be Subset of ( One-Point_Compactification X) such that

       A13: X9 = ( [#] X) and

       A14: X9 is dense;

      

       A15: ( Cl X9) = ( [#] ( One-Point_Compactification X)) by A14;

      assume X is compact;

      then ( [#] X) is compact;

      then (( {} X) ` ) is compact;

      then (( {} X) \/ {( [#] X)}) in D;

      then

       A16: {( [#] X)} in the topology of ( One-Point_Compactification X) by A5, XBOOLE_0:def 3;

      then

      reconsider X1 = {( [#] X)} as Subset of ( One-Point_Compactification X);

      X1 is open by A16;

      then

       A17: ( Cl (X1 ` )) = (X1 ` ) by PRE_TOPC: 22;

      (X1 ` ) = (( [#] X) \ X1) by A2, XBOOLE_1: 40

      .= ( [#] X) by A1, ZFMISC_1: 57;

      hence contradiction by A13, A15, A17, A4;

    end;

    theorem :: COMPACT1:8

    for X be non empty TopSpace st X is non compact holds ( incl (X,( One-Point_Compactification X))) is compactification

    proof

      let X be non empty TopSpace;

      set h = ( incl (X,( One-Point_Compactification X)));

      set D = { (U \/ {( [#] X)}) where U be Subset of X : U is open & (U ` ) is compact };

      assume X is non compact;

      then

       A1: ex X9 be Subset of ( One-Point_Compactification X) st X9 = ( [#] X) & X9 is dense by Th7;

      

       A2: ( [#] X) c= ( [#] ( One-Point_Compactification X)) by Th4;

      then

      reconsider Xy = ( [#] X) as Subset of ( One-Point_Compactification X);

      

       A3: ( [#] (( One-Point_Compactification X) | Xy)) = Xy by PRE_TOPC:def 5;

      

       A4: the topology of ( One-Point_Compactification X) = (the topology of X \/ D) by Def9;

      the topology of (( One-Point_Compactification X) | Xy) = the topology of X

      proof

        thus the topology of (( One-Point_Compactification X) | Xy) c= the topology of X

        proof

          let x be object;

          assume

           A5: x in the topology of (( One-Point_Compactification X) | Xy);

          then

          reconsider P = x as Subset of (( One-Point_Compactification X) | Xy);

          consider Q be Subset of ( One-Point_Compactification X) such that

           A6: Q in the topology of ( One-Point_Compactification X) and

           A7: P = (Q /\ ( [#] (( One-Point_Compactification X) | Xy))) by A5, PRE_TOPC:def 4;

          per cases by A4, A6, XBOOLE_0:def 3;

            suppose Q in the topology of X;

            hence thesis by A3, A7, XBOOLE_1: 28;

          end;

            suppose Q in D;

            then

            consider U be Subset of X such that

             A8: Q = (U \/ {( [#] X)}) and

             A9: U is open and (U ` ) is compact;

             not ( [#] X) in ( [#] X);

            then {( [#] X)} misses ( [#] X) by ZFMISC_1: 50;

            then ( {( [#] X)} /\ ( [#] X)) = {} ;

            

            then P = ((U /\ ( [#] X)) \/ {} ) by A3, A7, A8, XBOOLE_1: 23

            .= U by XBOOLE_1: 28;

            hence thesis by A9;

          end;

        end;

        let x be object;

        assume

         A10: x in the topology of X;

        then

        reconsider P = x as Subset of (( One-Point_Compactification X) | Xy) by A3;

        reconsider Q = P as Subset of ( One-Point_Compactification X) by A3, XBOOLE_1: 1;

        

         A11: P = (Q /\ ( [#] (( One-Point_Compactification X) | Xy))) by XBOOLE_1: 28;

        Q in the topology of ( One-Point_Compactification X) by A4, A10, XBOOLE_0:def 3;

        hence thesis by A11, PRE_TOPC:def 4;

      end;

      hence h is embedding by A2, Th3;

      thus ( One-Point_Compactification X) is compact;

      thus thesis by A1, Th2;

    end;