:: COMPACT1 semantic presentation

begin

definition
let X be TopSpace;
let P be Subset-Family of X;
attrP is compact  means :Def1: :: COMPACT1:def 1
 for U being Subset of X st U in P holds
U is compact ;
end;

:: deftheorem Def1 defines compact COMPACT1:def_1_:_
 for X being TopSpace
for P being Subset-Family of X holds
( P is compact iff for U being Subset of X st U in P holds
U is compact );

definition
let X be TopSpace;
let U be Subset of X;
attrU is relatively-compact  means :Def2: :: COMPACT1:def 2
 Cl U is compact ;
end;

:: deftheorem Def2 defines relatively-compact COMPACT1:def_2_:_
 for X being TopSpace
for U being Subset of X holds
( U is relatively-compact iff Cl U is compact );

registration
let X be TopSpace;
cluster empty  ->  relatively-compact for Element of K19( the carrier of X);
coherence
 for b1 being Subset of X st b1 is empty holds
b1 is relatively-compact
proof
let S be Subset of X; ::_thesis: ( S is empty implies S is relatively-compact )
assume A1: S is empty ; ::_thesis: S is relatively-compact
then  Cl S = S by PRE_TOPC:22;
hence  S is relatively-compact by A1, Def2; ::_thesis: verum
end;
end;

registration
let T be TopSpace;
cluster relatively-compact for Element of K19( the carrier of T);
existence
 ex b1 being Subset of T st b1 is relatively-compact
proof
take  {} T ; ::_thesis: {} T is relatively-compact
thus  {} T is relatively-compact ; ::_thesis: verum
end;
end;

registration
let X be TopSpace;
let U be relatively-compact Subset of X;
cluster Cl U ->  compact ;
coherence
 Cl U is compact by Def2;
end;

notation
let X be TopSpace;
let U be Subset of X;
synonym  pre-compact U for  relatively-compact ;
end;

notation
let X be non empty TopSpace;
synonym  liminally-compact X for  locally-compact ;
end;

definition
let X be non empty TopSpace;
redefine attr X is locally-compact  means :Def3: :: COMPACT1:def 3
 for x being Point of X ex B being basis of x st B is compact ;
compatibility
 ( X is liminally-compact iff for x being Point of X ex B being basis of x st B is compact )
proof
hereby  ::_thesis: ( ( for x being Point of X ex B being basis of x st B is compact ) implies X is liminally-compact )
assume A1: X is liminally-compact ; ::_thesis: for x being Point of X ex B being basis of x st B is compact
let x be Point of X; ::_thesis: ex B being basis of x st B is compact
set B =  {  Q where Q is a_neighborhood of x : ( Q is compact & ex V being a_neighborhood of x st Q c= V )  }  ;
  {  Q where Q is a_neighborhood of x : ( Q is compact & ex V being a_neighborhood of x st Q c= V )  }  c= bool ([#] X)
proof
let A be set ; :: according to TARSKI:def_3 ::_thesis: ( not A in  {  Q where Q is a_neighborhood of x : ( Q is compact & ex V being a_neighborhood of x st Q c= V )  }  or A in bool ([#] X) )
assume  A in  {  Q where Q is a_neighborhood of x : ( Q is compact & ex V being a_neighborhood of x st Q c= V )  }  ; ::_thesis: A in bool ([#] X)
then  ex Q being a_neighborhood of x st
( A = Q & Q is compact & ex V being a_neighborhood of x st Q c= V ) ;
hence  A in bool ([#] X) ; ::_thesis: verum
end;
then reconsider B =  {  Q where Q is a_neighborhood of x : ( Q is compact & ex V being a_neighborhood of x st Q c= V )  }  as Subset-Family of X ;
A2: B is basis of x
proof
let V be a_neighborhood of x; :: according to YELLOW13:def_2 ::_thesis: ex b1 being a_neighborhood of x st
( b1 in B & b1 c= V )
 x in Int V by CONNSP_2:def_1;
then consider Q being Subset of X such that
A3: x in Int Q and
A4: Q c= Int V and
A5: Q is compact by A1, WAYBEL_3:def_9;
reconsider Q = Q as a_neighborhood of x by A3, CONNSP_2:def_1;
take  Q ; ::_thesis: ( Q in B & Q c= V )
 Int V c= V by TOPS_1:16;
hence  ( Q in B & Q c= V ) by A4, A5, XBOOLE_1:1; ::_thesis: verum
end;
 B is compact
proof
let U be Subset of X; :: according to COMPACT1:def_1 ::_thesis: ( U in B implies U is compact )
assume  U in B ; ::_thesis: U is compact
then  ex Q being a_neighborhood of x st
( U = Q & Q is compact & ex V being a_neighborhood of x st Q c= V ) ;
hence  U is compact ; ::_thesis: verum
end;
hence  ex B being basis of x st B is compact by A2; ::_thesis: verum
end;
assume A6: for x being Point of X ex B being basis of x st B is compact ; ::_thesis: X is liminally-compact
let x be Point of X; :: according to WAYBEL_3:def_9 ::_thesis: for b1 being Element of K19( the carrier of X) holds
( not x in b1 or not b1 is open or ex b2 being Element of K19( the carrier of X) st
( x in Int b2 & b2 c= b1 & b2 is compact ) )
let P be Subset of X; ::_thesis: ( not x in P or not P is open or ex b1 being Element of K19( the carrier of X) st
( x in Int b1 & b1 c= P & b1 is compact ) )
assume that
A7: x in P and
A8: P is open ; ::_thesis: ex b1 being Element of K19( the carrier of X) st
( x in Int b1 & b1 c= P & b1 is compact )
consider B being basis of x such that
A9: B is compact by A6;
 x in Int P by A7, A8, TOPS_1:23;
then consider Q being 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 ; ::_thesis: ( x in Int Q & Q c= P & Q is compact )
thus  ( x in Int Q & Q c= P ) by A11, A12; ::_thesis: Q is compact
thus  Q is compact by A9, A10, Def1; ::_thesis: verum
end;
end;

:: deftheorem Def3 defines liminally-compact COMPACT1:def_3_:_
 for X being non empty TopSpace holds
( X is liminally-compact iff for x being Point of X ex B being basis of x st B is compact );

definition
let X be non empty TopSpace;
attrX is locally-relatively-compact  means :Def4: :: COMPACT1:def 4
 for x being Point of X ex U being a_neighborhood of x st U is relatively-compact ;
end;

:: deftheorem Def4 defines locally-relatively-compact COMPACT1:def_4_:_
 for X being non empty TopSpace holds
( X is locally-relatively-compact iff for x being Point of X ex U being a_neighborhood of x st U is relatively-compact );

definition
let X be non empty TopSpace;
attrX is locally-closed/compact  means :Def5: :: COMPACT1:def 5
 for x being Point of X ex U being a_neighborhood of x st
( U is closed & U is compact );
end;

:: deftheorem Def5 defines locally-closed/compact COMPACT1:def_5_:_
 for X being non empty TopSpace holds
( X is locally-closed/compact iff for x being Point of X ex U being a_neighborhood of x st
( U is closed & U is compact ) );

definition
let X be non empty TopSpace;
attrX is locally-compact  means :Def6: :: COMPACT1:def 6
 for x being Point of X ex U being a_neighborhood of x st U is compact ;
end;

:: deftheorem Def6 defines locally-compact COMPACT1:def_6_:_
 for X being non empty TopSpace holds
( X is locally-compact iff for x being Point of X ex U being a_neighborhood of x st U is compact );

registration
cluster non empty TopSpace-like liminally-compact  ->  non empty locally-compact for TopStruct ;
coherence
 for b1 being non empty TopSpace st b1 is liminally-compact holds
b1 is locally-compact
proof
let X be non empty TopSpace; ::_thesis: ( X is liminally-compact implies X is locally-compact )
assume A1: X is liminally-compact ; ::_thesis: X is locally-compact
let x be Point of X; :: according to COMPACT1:def_6 ::_thesis: ex U being a_neighborhood of x st U is compact
consider B being basis of x such that
A2: B is compact by A1, Def3;
set V = the a_neighborhood of x;
consider Y being a_neighborhood of x such that
A3: Y in B and
 Y c= the a_neighborhood of x by YELLOW13:def_2;
 Y is compact by A2, A3, Def1;
hence  ex U being a_neighborhood of x st U is compact ; ::_thesis: verum
end;
end;

registration
cluster non empty TopSpace-like regular locally-compact  ->  non empty regular liminally-compact for TopStruct ;
coherence
 for b1 being non empty regular TopSpace st b1 is locally-compact holds
b1 is liminally-compact
proof
let X be non empty regular TopSpace; ::_thesis: ( X is locally-compact implies X is liminally-compact )
assume A1: X is locally-compact ; ::_thesis: X is liminally-compact
let x be Point of X; :: according to COMPACT1:def_3 ::_thesis: ex B being basis of x st B is compact
set B =  {  Q where Q is a_neighborhood of x : ( Q is compact & ex V, W being a_neighborhood of x st Q c= V /\ W )  }  ;
  {  Q where Q is a_neighborhood of x : ( Q is compact & ex V, W being a_neighborhood of x st Q c= V /\ W )  }  c= bool ([#] X)
proof
let A be set ; :: according to TARSKI:def_3 ::_thesis: ( not A in  {  Q where Q is a_neighborhood of x : ( Q is compact & ex V, W being a_neighborhood of x st Q c= V /\ W )  }  or A in bool ([#] X) )
assume  A in  {  Q where Q is a_neighborhood of x : ( Q is compact & ex V, W being a_neighborhood of x st Q c= V /\ W )  }  ; ::_thesis: A in bool ([#] X)
then  ex Q being a_neighborhood of x st
( A = Q & Q is compact & ex V, W being a_neighborhood of x st Q c= V /\ W ) ;
hence  A in bool ([#] X) ; ::_thesis: verum
end;
then reconsider B =  {  Q where Q is a_neighborhood of x : ( Q is compact & ex V, W being a_neighborhood of x st Q c= V /\ W )  }  as Subset-Family of X ;
A2: B is basis of x
proof
let V be a_neighborhood of x; :: according to YELLOW13:def_2 ::_thesis: ex b1 being a_neighborhood of x st
( b1 in B & b1 c= V )
A3: x in Int V by CONNSP_2:def_1;
consider W being a_neighborhood of x such that
A4: W is compact by A1, Def6;
 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 being 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 = Q as a_neighborhood of x by A7, CONNSP_2:def_1;
take  Q ; ::_thesis: ( Q in B & Q c= V )
 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; ::_thesis: Q c= V
 V /\ W c= V by XBOOLE_1:17;
hence  Q c= V by A6, XBOOLE_1:1; ::_thesis: verum
end;
 B is compact
proof
let U be Subset of X; :: according to COMPACT1:def_1 ::_thesis: ( U in B implies U is compact )
assume  U in B ; ::_thesis: U is compact
then  ex Q being a_neighborhood of x st
( U = Q & Q is compact & ex V, W being a_neighborhood of x st Q c= V /\ W ) ;
hence  U is compact ; ::_thesis: verum
end;
hence  ex B being basis of x st B is compact by A2; ::_thesis: verum
end;
end;

registration
cluster non empty TopSpace-like locally-relatively-compact  ->  non empty locally-closed/compact for TopStruct ;
coherence
 for b1 being non empty TopSpace st b1 is locally-relatively-compact holds
b1 is locally-closed/compact
proof
let X be non empty TopSpace; ::_thesis: ( X is locally-relatively-compact implies X is locally-closed/compact )
assume A1: X is locally-relatively-compact ; ::_thesis: X is locally-closed/compact
let x be Point of X; :: according to COMPACT1:def_5 ::_thesis: ex U being a_neighborhood of x st
( U is closed & U is compact )
consider U being a_neighborhood of x such that
A2: U is relatively-compact by A1, Def4;
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  ex U being a_neighborhood of x st
( U is closed & U is compact ) by A2; ::_thesis: verum
end;
end;

registration
cluster non empty TopSpace-like locally-closed/compact  ->  non empty locally-relatively-compact for TopStruct ;
coherence
 for b1 being non empty TopSpace st b1 is locally-closed/compact holds
b1 is locally-relatively-compact
proof
let X be non empty TopSpace; ::_thesis: ( X is locally-closed/compact implies X is locally-relatively-compact )
assume A1: X is locally-closed/compact ; ::_thesis: X is locally-relatively-compact
let x be Point of X; :: according to COMPACT1:def_4 ::_thesis: ex U being a_neighborhood of x st U is relatively-compact
consider U being a_neighborhood of x such that
A2: ( U is closed & U is compact ) by A1, Def5;
 Cl U = U by A2, PRE_TOPC:22;
then  U is relatively-compact by A2, Def2;
hence  ex U being a_neighborhood of x st U is relatively-compact ; ::_thesis: verum
end;
end;

registration
cluster non empty TopSpace-like locally-relatively-compact  ->  non empty locally-compact for TopStruct ;
coherence
 for b1 being non empty TopSpace st b1 is locally-relatively-compact holds
b1 is locally-compact
proof
let X be non empty TopSpace; ::_thesis: ( X is locally-relatively-compact implies X is locally-compact )
assume A1: X is locally-relatively-compact ; ::_thesis: X is locally-compact
let x be Point of X; :: according to COMPACT1:def_6 ::_thesis: ex U being a_neighborhood of x st U is compact
consider Y being a_neighborhood of x such that
A2: Y is relatively-compact by A1, Def4;
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  ex U being a_neighborhood of x st U is compact by A2; ::_thesis: verum
end;
end;

registration
cluster non empty TopSpace-like Hausdorff locally-compact  ->  non empty Hausdorff locally-relatively-compact for TopStruct ;
coherence
 for b1 being non empty Hausdorff TopSpace st b1 is locally-compact holds
b1 is locally-relatively-compact
proof
let X be non empty Hausdorff TopSpace; ::_thesis: ( X is locally-compact implies X is locally-relatively-compact )
assume A1: X is locally-compact ; ::_thesis: X is locally-relatively-compact
let x be Point of X; :: according to COMPACT1:def_4 ::_thesis: ex U being a_neighborhood of x st U is relatively-compact
consider U being a_neighborhood of x such that
A2: U is compact by A1, Def6;
 Cl U = U by A2, PRE_TOPC:22;
then  U is relatively-compact by A2, Def2;
hence  ex U being a_neighborhood of x st U is relatively-compact ; ::_thesis: verum
end;
end;

registration
cluster non empty TopSpace-like compact  ->  non empty locally-compact for TopStruct ;
coherence
 for b1 being non empty TopSpace st b1 is compact holds
b1 is locally-compact
proof
let X be non empty TopSpace; ::_thesis: ( X is compact implies X is locally-compact )
set Y = [#] X;
assume A1: X is compact ; ::_thesis: X is locally-compact
let x be Point of X; :: according to COMPACT1:def_6 ::_thesis: ex U being a_neighborhood of x st U is compact
 Int ([#] X) = [#] X by TOPS_1:23;
then  [#] X is a_neighborhood of x by CONNSP_2:def_1;
hence  ex U being a_neighborhood of x st U is compact by A1; ::_thesis: verum
end;
end;

registration
cluster non empty TopSpace-like discrete  ->  non empty locally-compact for TopStruct ;
coherence
 for b1 being non empty TopSpace st b1 is discrete holds
b1 is locally-compact
proof
let X be non empty TopSpace; ::_thesis: ( X is discrete implies X is locally-compact )
assume A1: X is discrete ; ::_thesis: X is locally-compact
let x be Point of X; :: according to COMPACT1:def_6 ::_thesis: ex U being a_neighborhood of x st U is compact
set Y = {x};
 {x} is open by A1, TDLAT_3:15;
then  Int {x} = {x} by TOPS_1:23;
then  x in Int {x} by TARSKI:def_1;
then reconsider Y = {x} as a_neighborhood of x by CONNSP_2:def_1;
 Y is compact ;
hence  ex U being a_neighborhood of x st U is compact ; ::_thesis: verum
end;
end;

registration
cluster non empty TopSpace-like discrete for TopStruct ;
existence
 ex b1 being TopSpace st
( b1 is discrete & not b1 is empty )
proof
set X = the non empty discrete TopSpace;
take  the non empty discrete TopSpace ; ::_thesis: ( the non empty discrete TopSpace is discrete & not the non empty discrete TopSpace is empty )
thus  ( the non empty discrete TopSpace is discrete & not the non empty discrete TopSpace is empty ) ; ::_thesis: verum
end;
end;

registration
let X be non empty locally-compact TopSpace;
let C be non empty closed Subset of X;
clusterX | C ->  locally-compact ;
coherence
 X | C is locally-compact
proof
let x be Point of (X | C); :: according to COMPACT1:def_6 ::_thesis: ex U being a_neighborhood of x st U is compact
reconsider xx = x as Point of X by PRE_TOPC:25;
consider K being 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 = KC as a_neighborhood of x by A2, TOPMETR:5;
take  KC ; ::_thesis: KC is compact
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  KC is compact by A7, COMPTS_1:3; ::_thesis: verum
end;
end;

registration
let X be non empty regular locally-compact TopSpace;
let P be non empty open Subset of X;
clusterX | P ->  locally-compact ;
coherence
 X | P is locally-compact
proof
let x be Point of (X | P); :: according to COMPACT1:def_6 ::_thesis: ex U being a_neighborhood of x st U is compact
reconsider xx = x as Point of X by PRE_TOPC:25;
consider B being 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 being 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, Def1;
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  ex U being a_neighborhood of x st U is compact by A5; ::_thesis: verum
end;
end;

theorem :: COMPACT1:1
for X being non empty Hausdorff TopSpace
for E being non empty Subset of X st X | E is dense & X | E is locally-compact holds
X | E is open
proof
let X be non empty Hausdorff TopSpace; ::_thesis: for E being non empty Subset of X st X | E is dense & X | E is locally-compact holds
X | E is open
let E be non empty Subset of X; ::_thesis: ( X | E is dense & X | E is locally-compact implies X | E is open )
assume A1: ( X | E is dense & X | E is locally-compact ) ; ::_thesis: X | E is open
A2: [#] (X | E) = E by PRE_TOPC:8;
 Int E = E
proof
thus  Int E c= E by TOPS_1:16; :: according to XBOOLE_0:def_10 ::_thesis: E c= Int E
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in E or a in Int E )
assume A3: a in E ; ::_thesis: a in Int 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 is Subset of X : ( G is open & G c= E )  }  ;
consider K being a_neighborhood of xx such that
A4: K is compact by A1, Def6;
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 being 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, PRE_TOPC:def_2;
 for P being 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, XBOOLE_1:1;
then  G c= E by A2, XBOOLE_1:1;
then A11: G in  {  G where G is Subset of X : ( G is open & G c= E )  }  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  {  G where G is Subset of X : ( G is open & G c= E )  }  by A12, A11, TARSKI:def_4;
hence  a in Int E by TEX_4:3; ::_thesis: verum
end;
hence  X | E is open by A2, TSEP_1:16; ::_thesis: verum
end;

theorem Th2: :: COMPACT1:2
for X, Y being TopSpace
for A being Subset of X st [#] X c= [#] Y holds
(incl (X,Y)) .: A = A
proof
let X, Y be TopSpace; ::_thesis: for A being Subset of X st [#] X c= [#] Y holds
(incl (X,Y)) .: A = A
let A be Subset of X; ::_thesis: ( [#] X c= [#] Y implies (incl (X,Y)) .: A = A )
assume  [#] X c= [#] Y ; ::_thesis: (incl (X,Y)) .: A = A
hence (incl (X,Y)) .: A = (id ([#] X)) .: A by YELLOW_9:def_1
.= A by FUNCT_1:92 ;
::_thesis: verum
end;

definition
let X, Y be TopSpace;
let f be Function of X,Y;
attrf is embedding  means :: COMPACT1:def 7
 ex h being Function of X,(Y | (rng f)) st
( h = f & h is being_homeomorphism );
end;

:: deftheorem  defines embedding COMPACT1:def_7_:_
 for X, Y being TopSpace
for f being Function of X,Y holds
( f is embedding iff ex h being Function of X,(Y | (rng f)) st
( h = f & h is being_homeomorphism ) );

theorem Th3: :: COMPACT1:3
for X, Y being TopSpace st [#] X c= [#] Y & ex Xy being 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; ::_thesis: ( [#] X c= [#] Y & ex Xy being Subset of Y st
( Xy = [#] X & the topology of (Y | Xy) = the topology of X ) implies incl (X,Y) is embedding )
assume A1: [#] X c= [#] Y ; ::_thesis: ( for Xy being Subset of Y holds
( not Xy = [#] X or not the topology of (Y | Xy) = the topology of X ) or incl (X,Y) is embedding )
A2: incl (X,Y) = id X by A1, YELLOW_9:def_1;
set YY = Y | (rng (incl (X,Y)));
A3: [#] (Y | (rng (incl (X,Y)))) = 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,(Y | (rng (incl (X,Y)))) by A3, FUNCT_2:6;
set f = id X;
given Xy being Subset of Y such that A5: Xy = [#] X and
A6: the topology of (Y | Xy) = the topology of X ; ::_thesis: incl (X,Y) is embedding
A7: for P being Subset of X st P is open holds
(h ") " P is open
proof
let P be Subset of X; ::_thesis: ( P is open implies (h ") " P is open )
reconsider Q = P as Subset of (Y | (rng (incl (X,Y)))) by A2, A3, RELAT_1:45;
assume  P is open ; ::_thesis: (h ") " P is open
then A8: P in the topology of X by PRE_TOPC:def_2;
(h ") " P = h .: Q by A2, A3, TOPS_2:54
.= Q by A2, FUNCT_1:92 ;
hence  (h ") " P in the topology of (Y | (rng (incl (X,Y)))) by A5, A6, A2, A8, RELAT_1:45; :: according to PRE_TOPC:def_2 ::_thesis: verum
end;
A9: ( [#] X = {} implies [#] X = {} ) ;
A10: for P being Subset of (Y | (rng (incl (X,Y)))) st P is open holds
h " P is open
proof
let P be Subset of (Y | (rng (incl (X,Y)))); ::_thesis: ( P is open implies h " P is open )
reconsider Q = P as Subset of X by A2, A3, RELAT_1:45;
assume  P is open ; ::_thesis: h " P is open
then  P in the topology of (Y | (rng (incl (X,Y)))) by PRE_TOPC:def_2;
then  Q in the topology of X by A5, A6, A2, RELAT_1:45;
then  Q is open by PRE_TOPC:def_2;
then  (id X) " Q is open by A9, TOPS_2:43;
then  (id X) " Q in the topology of X by PRE_TOPC:def_2;
hence  h " P in the topology of X by A1, YELLOW_9:def_1; :: according to PRE_TOPC:def_2 ::_thesis: verum
end;
take  h ; :: according to COMPACT1:def_7 ::_thesis: ( h = incl (X,Y) & h is being_homeomorphism )
thus  h = incl (X,Y) ; ::_thesis: h is being_homeomorphism
thus  ( dom h = [#] X & rng h = [#] (Y | (rng (incl (X,Y)))) ) by A4, FUNCT_2:def_1, PRE_TOPC:def_5; :: according to TOPS_2:def_5 ::_thesis: ( h is one-to-one & h is continuous & h " is continuous )
thus  h is one-to-one by A2; ::_thesis: ( h is continuous & h " is continuous )
 ( [#] (Y | (rng (incl (X,Y)))) = {} implies [#] X = {} ) by A2, A3;
hence  h is continuous by A10, TOPS_2:43; ::_thesis: h " is continuous
 ( [#] X = {} implies [#] (Y | (rng (incl (X,Y)))) = {} ) ;
hence  h " is continuous by A7, TOPS_2:43; ::_thesis: verum
end;

definition
let X, Y be TopSpace;
let h be Function of X,Y;
attrh is compactification  means :Def8: :: COMPACT1:def 8
( h is embedding & Y is compact & h .: ([#] X) is dense );
end;

:: deftheorem Def8 defines compactification COMPACT1:def_8_:_
 for X, Y being TopSpace
for h being Function of X,Y holds
( h is compactification iff ( h is embedding & Y is compact & h .: ([#] X) is dense ) );

registration
let X, Y be TopSpace;
cluster Function-like V18( the carrier of X, the carrier of Y) compactification  ->  embedding for Element of K19(K20( the carrier of X, the carrier of Y));
coherence
 for b1 being Function of X,Y st b1 is compactification holds
b1 is embedding by Def8;
end;

definition
let X be TopStruct ;
func One-Point_Compactification X ->  strict TopStruct  means :Def9: :: COMPACT1:def 9
( the carrier of it = succ ([#] X) & the topology of it = the topology of X \/  {  (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact )  }  );
existence
 ex b1 being strict TopStruct st
( the carrier of b1 = succ ([#] X) & the topology of b1 = the topology of X \/  {  (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact )  }  )
proof
set T = succ ([#] X);
set D =  {  (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact )  }  ;
set O = the topology of X \/  {  (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact )  }  ;
 the topology of X \/  {  (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact )  }  c= bool (succ ([#] X))
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in the topology of X \/  {  (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact )  }  or a in bool (succ ([#] X)) )
A1: now__::_thesis:_(_a_in__{__(U_\/_{([#]_X)})_where_U_is_Subset_of_X_:_(_U_is_open_&_U_`_is_compact_)__}__implies_a_c=_succ_([#]_X)_)
assume  a in  {  (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact )  }  ; ::_thesis: a c= succ ([#] X)
then consider U being Subset of X such that
A2: a = U \/ {([#] X)} and
 U is open and
 U ` is compact ;
thus  a c= succ ([#] X) ::_thesis: verum
proof
let A be set ; :: according to TARSKI:def_3 ::_thesis: ( not A in a or A in succ ([#] X) )
assume  A in a ; ::_thesis: A in succ ([#] X)
then  ( A in U or A in {([#] X)} ) by A2, XBOOLE_0:def_3;
hence  A in succ ([#] X) by XBOOLE_0:def_3; ::_thesis: verum
end;
end;
assume  a in the topology of X \/  {  (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact )  }  ; ::_thesis: a in bool (succ ([#] X))
then  ( a in the topology of X or a in  {  (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact )  }  ) by XBOOLE_0:def_3;
then  a is Subset of (succ ([#] X)) by A1, XBOOLE_1:10;
hence  a in bool (succ ([#] X)) ; ::_thesis: verum
end;
then reconsider O = the topology of X \/  {  (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact )  }  as Subset-Family of (succ ([#] X)) ;
set Y = TopStruct(# (succ ([#] X)),O #);
 not TopStruct(# (succ ([#] X)),O #) is empty ;
hence  ex b1 being strict TopStruct st
( the carrier of b1 = succ ([#] X) & the topology of b1 = the topology of X \/  {  (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact )  }  ) ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being strict TopStruct st the carrier of b1 = succ ([#] X) & the topology of b1 = the topology of X \/  {  (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact )  }  & the carrier of b2 = succ ([#] X) & the topology of b2 = the topology of X \/  {  (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact )  }  holds
b1 = b2 ;
end;

:: deftheorem Def9 defines One-Point_Compactification COMPACT1:def_9_:_
 for X being TopStruct
for b2 being strict TopStruct holds
( b2 = One-Point_Compactification X iff ( the carrier of b2 = succ ([#] X) & the topology of b2 = the topology of X \/  {  (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact )  }  ) );

registration
let X be TopStruct ;
cluster One-Point_Compactification X ->  non empty strict ;
coherence
 not One-Point_Compactification X is empty
proof
 the carrier of (One-Point_Compactification X) = succ ([#] X) by Def9;
hence  not One-Point_Compactification X is empty ; ::_thesis: verum
end;
end;

theorem Th4: :: COMPACT1:4
for X being TopStruct holds [#] X c= [#] (One-Point_Compactification X)
proof
let X be TopStruct ; ::_thesis: [#] X c= [#] (One-Point_Compactification X)
 [#] (One-Point_Compactification X) = succ ([#] X) by Def9;
hence  [#] X c= [#] (One-Point_Compactification X) by XBOOLE_1:7; ::_thesis: verum
end;

registration
let X be TopSpace;
cluster One-Point_Compactification X ->  strict TopSpace-like ;
coherence
 One-Point_Compactification X is TopSpace-like
proof
set Y = One-Point_Compactification X;
set T = succ ([#] X);
set D =  {  (U \/ {([#] X)}) where U is 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 \/  {  (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact )  }  by Def9;
A3: [#] (One-Point_Compactification X) = succ ([#] X) by Def9;
 One-Point_Compactification X is TopSpace-like
proof
([#] X) ` = (({} X) `) `
.= {} X ;
then  succ ([#] X) in  {  (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact )  }  ;
hence  the carrier of (One-Point_Compactification X) in the topology of (One-Point_Compactification X) by A3, A2, XBOOLE_0:def_3; :: according to PRE_TOPC:def_1 ::_thesis: ( ( for b1 being Element of K19(K19( the carrier of (One-Point_Compactification X))) holds
( not b1 c= the topology of (One-Point_Compactification X) or union b1 in the topology of (One-Point_Compactification X) ) ) & ( for b1, b2 being Element of K19( the carrier of (One-Point_Compactification X)) holds
( not b1 in the topology of (One-Point_Compactification X) or not b2 in the topology of (One-Point_Compactification X) or b1 /\ b2 in the topology of (One-Point_Compactification X) ) ) )
hereby  ::_thesis: for b1, b2 being Element of K19( the carrier of (One-Point_Compactification X)) holds
( not b1 in the topology of (One-Point_Compactification X) or not b2 in the topology of (One-Point_Compactification X) or b1 /\ b2 in the topology of (One-Point_Compactification X) )
let a be Subset-Family of (One-Point_Compactification X); ::_thesis: ( a c= the topology of (One-Point_Compactification X) implies union b1 in the topology of (One-Point_Compactification X) )
A4: not [#] X in [#] X ;
set ua =  {  U where U is Subset of X : ( U is open & ( U in a or U \/ {([#] X)} in a ) )  }  ;
A5:  {  U where U is Subset of X : ( U is open & ( U in a or U \/ {([#] X)} in a ) )  }  c= the topology of X
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  U where U is Subset of X : ( U is open & ( U in a or U \/ {([#] X)} in a ) )  }  or x in the topology of X )
assume  x in  {  U where U is Subset of X : ( U is open & ( U in a or U \/ {([#] X)} in a ) )  }  ; ::_thesis: x in the topology of X
then  ex U being Subset of X st
( x = U & U is open & ( U in a or U \/ {([#] X)} in a ) ) ;
hence  x in the topology of X by PRE_TOPC:def_2; ::_thesis: verum
end;
then reconsider ua =  {  U where U is Subset of X : ( U is open & ( U in a or U \/ {([#] X)} in a ) )  }  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 by PRE_TOPC:def_2;
assume A7: a c= the topology of (One-Point_Compactification X) ; ::_thesis: union b1 in the topology of (One-Point_Compactification X)
A8: union ua = (union a) \ {([#] X)}
proof
thus  union ua c= (union a) \ {([#] X)} :: according to XBOOLE_0:def_10 ::_thesis: (union a) \ {([#] X)} c= union ua
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in union ua or x in (union a) \ {([#] X)} )
assume  x in union ua ; ::_thesis: x in (union a) \ {([#] X)}
then consider A being set  such that
A9: x in A and
A10: A in ua by TARSKI:def_4;
consider U being 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__::_thesis:_x_in_union_a
percases ( U in a or U \/ {([#] X)} in a ) by A12;
suppose U in a ; ::_thesis: x in union a
hence  x in union a by A9, A11, TARSKI:def_4; ::_thesis: verum
end;
supposeA14: U \/ {([#] X)} in a ; ::_thesis: x in union a
 x in U \/ {([#] X)} by A9, A11, XBOOLE_0:def_3;
hence  x in union a by A14, TARSKI:def_4; ::_thesis: verum
end;
end;
end;
now__::_thesis:_not_x_in_{([#]_X)}
assume  x in {([#] X)} ; ::_thesis: contradiction
then A15: x = [#] X by TARSKI:def_1;
 x in [#] X by A9, A11;
hence  contradiction by A15; ::_thesis: verum
end;
hence  x in (union a) \ {([#] X)} by A13, XBOOLE_0:def_5; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (union a) \ {([#] X)} or x in union ua )
assume A16: x in (union a) \ {([#] X)} ; ::_thesis: x in union ua
then  x in union a by XBOOLE_0:def_5;
then consider A being set  such that
A17: x in A and
A18: A in a by TARSKI:def_4;
percases ( A in the topology of X or A in  {  (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact )  }  ) by A2, A7, A18, XBOOLE_0:def_3;
supposeA19: A in the topology of X ; ::_thesis: x in union ua
then reconsider U = A as Subset of X ;
 U is open by A19, PRE_TOPC:def_2;
then  U in ua by A18;
hence  x in union ua by A17, TARSKI:def_4; ::_thesis: verum
end;
suppose A in  {  (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact )  }  ; ::_thesis: x in union ua
then consider U being 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  x in union ua by A22, TARSKI:def_4; ::_thesis: verum
end;
end;
end;
percases ( [#] X in union a or not [#] X in union a ) ;
supposeA23: [#] X in union a ; ::_thesis: union b1 in the topology of (One-Point_Compactification X)
then consider A being 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  {  (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact )  }  ) by A2, A7, A25, XBOOLE_0:def_3;
then consider U being Subset of X such that
A26: A = U \/ {([#] X)} and
 U is open and
A27: U ` is compact by A4, A24;
A28: now__::_thesis:_not_[#]_X_in_U
assume  [#] X in U ; ::_thesis: contradiction
then  [#] X in [#] X ;
hence  contradiction ; ::_thesis: verum
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  {  (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact )  }  by A6, A29;
hence  union a in the topology of (One-Point_Compactification X) by A2, XBOOLE_0:def_3; ::_thesis: verum
end;
supposeA30: not [#] X in union a ; ::_thesis: union b1 in the topology of (One-Point_Compactification X)
A31: a c= the topology of X
proof
let A be set ; :: according to TARSKI:def_3 ::_thesis: ( not A in a or A in the topology of X )
assume A32: A in a ; ::_thesis: A in the topology of X
assume  not A in the topology of X ; ::_thesis: contradiction
then  A in  {  (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact )  }  by A2, A7, A32, XBOOLE_0:def_3;
then A33: ex U being Subset of X st
( A = U \/ {([#] X)} & U is open & U ` is compact ) ;
 [#] X in {([#] X)} by TARSKI:def_1;
then  [#] X in A by A33, XBOOLE_0:def_3;
hence  contradiction by A30, A32, TARSKI:def_4; ::_thesis: verum
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 (One-Point_Compactification X) by A2, XBOOLE_0:def_3; ::_thesis: verum
end;
end;
end;
let a, b be Subset of (One-Point_Compactification X); ::_thesis: ( not a in the topology of (One-Point_Compactification X) or not b in the topology of (One-Point_Compactification X) or a /\ b in the topology of (One-Point_Compactification X) )
assume A34: a in the topology of (One-Point_Compactification X) ; ::_thesis: ( not b in the topology of (One-Point_Compactification X) or a /\ b in the topology of (One-Point_Compactification X) )
assume A35: b in the topology of (One-Point_Compactification X) ; ::_thesis: a /\ b in the topology of (One-Point_Compactification X)
percases ( ( a in the topology of X & b in the topology of X ) or ( a in the topology of X & b in  {  (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact )  }  ) or ( b in the topology of X & a in  {  (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact )  }  ) or ( a in  {  (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact )  }  & b in  {  (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact )  }  ) ) by A2, A34, A35, XBOOLE_0:def_3;
suppose ( a in the topology of X & b in the topology of X ) ; ::_thesis: a /\ b in the topology of (One-Point_Compactification X)
then  a /\ b in the topology of X by PRE_TOPC:def_1;
hence  a /\ b in the topology of (One-Point_Compactification X) by A2, XBOOLE_0:def_3; ::_thesis: verum
end;
supposethat A36: a in the topology of X and
A37: b in  {  (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact )  }  ; ::_thesis: a /\ b in the topology of (One-Point_Compactification X)
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 by XBOOLE_0:def_7;
then reconsider aX = a9 /\ {([#] X)} as open Subset of X ;
consider U being 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, PRE_TOPC:def_2;
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 (One-Point_Compactification X) by A2, XBOOLE_0:def_3; ::_thesis: verum
end;
supposethat A40: b in the topology of X and
A41: a in  {  (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact )  }  ; ::_thesis: a /\ b in the topology of (One-Point_Compactification X)
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 by XBOOLE_0:def_7;
then reconsider bX = b9 /\ {([#] X)} as open Subset of X ;
consider U being 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, PRE_TOPC:def_2;
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 (One-Point_Compactification X) by A2, XBOOLE_0:def_3; ::_thesis: verum
end;
supposethat A44: a in  {  (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact )  }  and
A45: b in  {  (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact )  }  ; ::_thesis: a /\ b in the topology of (One-Point_Compactification X)
consider Ua being Subset of X such that
A46: a = Ua \/ {([#] X)} and
A47: Ua is open and
A48: Ua ` is compact by A44;
consider Ub being 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  {  (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact )  }  by A47, A50, A52;
hence  a /\ b in the topology of (One-Point_Compactification X) by A2, XBOOLE_0:def_3; ::_thesis: verum
end;
end;
end;
hence  One-Point_Compactification X is TopSpace-like ; ::_thesis: verum
end;
end;

theorem Th5: :: COMPACT1:5
for X being TopStruct holds X is SubSpace of One-Point_Compactification X
proof
let X be TopStruct ; ::_thesis: X is SubSpace of One-Point_Compactification X
set D =  {  (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact )  }  ;
thus A1: [#] X c= [#] (One-Point_Compactification X) by Th4; :: according to PRE_TOPC:def_4 ::_thesis: for b1 being Element of K19( the carrier of X) holds
( ( not b1 in the topology of X or ex b2 being Element of K19( the carrier of (One-Point_Compactification X)) st
( b2 in the topology of (One-Point_Compactification X) & b1 = b2 /\ ([#] X) ) ) & ( for b2 being Element of K19( the carrier of (One-Point_Compactification X)) holds
( not b2 in the topology of (One-Point_Compactification X) or not b1 = b2 /\ ([#] X) ) or b1 in the topology of X ) )
let P be Subset of X; ::_thesis: ( ( not P in the topology of X or ex b1 being Element of K19( the carrier of (One-Point_Compactification X)) st
( b1 in the topology of (One-Point_Compactification X) & P = b1 /\ ([#] X) ) ) & ( for b1 being Element of K19( the carrier of (One-Point_Compactification X)) holds
( not b1 in the topology of (One-Point_Compactification X) or not P = b1 /\ ([#] X) ) or P in the topology of X ) )
A2: the topology of (One-Point_Compactification X) = the topology of X \/  {  (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact )  }  by Def9;
hereby  ::_thesis: ( for b1 being Element of K19( the carrier of (One-Point_Compactification X)) holds
( not b1 in the topology of (One-Point_Compactification X) or not P = b1 /\ ([#] X) ) or P in the topology of X )
reconsider Q = P as Subset of (One-Point_Compactification X) by A1, XBOOLE_1:1;
assume A3: P in the topology of X ; ::_thesis: ex Q being Subset of (One-Point_Compactification X) st
( Q in the topology of (One-Point_Compactification X) & P = Q /\ ([#] X) )
take Q = Q; ::_thesis: ( Q in the topology of (One-Point_Compactification X) & P = Q /\ ([#] X) )
thus  Q in the topology of (One-Point_Compactification X) by A2, A3, XBOOLE_0:def_3; ::_thesis: P = Q /\ ([#] X)
thus  P = Q /\ ([#] X) by XBOOLE_1:28; ::_thesis: verum
end;
given Q being Subset of (One-Point_Compactification X) such that A4: Q in the topology of (One-Point_Compactification X) and
A5: P = Q /\ ([#] X) ; ::_thesis: P in the topology of X
percases ( Q in the topology of X or Q in  {  (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact )  }  ) by A2, A4, XBOOLE_0:def_3;
suppose Q in the topology of X ; ::_thesis: P in the topology of X
hence  P in the topology of X by A5, XBOOLE_1:28; ::_thesis: verum
end;
suppose Q in  {  (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact )  }  ; ::_thesis: P in the topology of X
then consider U being 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) = {} by XBOOLE_0:def_7;
then P = (U /\ ([#] X)) \/ {} by A5, A6, XBOOLE_1:23
.= U by XBOOLE_1:28 ;
hence  P in the topology of X by A7, PRE_TOPC:def_2; ::_thesis: verum
end;
end;
end;

registration
let X be TopSpace;
cluster One-Point_Compactification X ->  strict compact ;
coherence
 One-Point_Compactification X is compact
proof
set D =  {  (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact )  }  ;
let F be Subset-Family of (One-Point_Compactification X); :: according to COMPTS_1:def_1 ::_thesis: ( not F is Cover of the carrier of (One-Point_Compactification X) or not F is open or ex b1 being Element of K19(K19( the carrier of (One-Point_Compactification X))) st
( b1 c= F & b1 is Cover of the carrier of (One-Point_Compactification X) & b1 is finite ) )
assume that
A1: F is Cover of (One-Point_Compactification X) and
A2: F is open ; ::_thesis: ex b1 being Element of K19(K19( the carrier of (One-Point_Compactification X))) st
( b1 c= F & b1 is Cover of the carrier of (One-Point_Compactification X) & b1 is finite )
A3: [#] (One-Point_Compactification X) c= union F by A1, SETFAM_1:def_11;
set Fx =  {  U where U is Subset of X : ( U is open & ( ( U in F & not U \/ {([#] X)} in F ) or U \/ {([#] X)} in F ) )  }  ;
  {  U where U is Subset of X : ( U is open & ( ( U in F & not U \/ {([#] X)} in F ) or U \/ {([#] X)} in F ) )  }  c= the topology of X
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  U where U is Subset of X : ( U is open & ( ( U in F & not U \/ {([#] X)} in F ) or U \/ {([#] X)} in F ) )  }  or x in the topology of X )
assume  x in  {  U where U is Subset of X : ( U is open & ( ( U in F & not U \/ {([#] X)} in F ) or U \/ {([#] X)} in F ) )  }  ; ::_thesis: x in the topology of X
then  ex U being Subset of X st
( x = U & U is open & ( ( U in F & not U \/ {([#] X)} in F ) or U \/ {([#] X)} in F ) ) ;
hence  x in the topology of X by PRE_TOPC:def_2; ::_thesis: verum
end;
then reconsider Fx =  {  U where U is Subset of X : ( U is open & ( ( U in F & not U \/ {([#] X)} in F ) or U \/ {([#] X)} in F ) )  }  as Subset-Family of X by XBOOLE_1:1;
A4: Fx is open
proof
let P be Subset of X; :: according to TOPS_2:def_1 ::_thesis: ( not P in Fx or P is open )
assume  P in Fx ; ::_thesis: P is open
then  ex U being Subset of X st
( P = U & U is open & ( ( U in F & not U \/ {([#] X)} in F ) or U \/ {([#] X)} in F ) ) ;
hence  P is open ; ::_thesis: verum
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 being set  such that
A5: [#] X in A and
A6: A in F by A3, TARSKI:def_4;
reconsider A = A as Subset of (One-Point_Compactification X) by A6;
 A is open by A2, A6, TOPS_2:def_1;
then  A in the topology of (One-Point_Compactification X) by PRE_TOPC:def_2;
then A7: A in the topology of X \/  {  (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact )  }  by Def9;
 not [#] X in [#] X ;
then  not A in the topology of X by A5;
then  A in  {  (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact )  }  by A7, XBOOLE_0:def_3;
then consider U being 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 set ; :: according to TARSKI:def_3,SETFAM_1:def_11 ::_thesis: ( not x in the carrier of X or x in union Fx )
assume A10: x in the carrier of X ; ::_thesis: x in union Fx
then  x in succ ([#] X) by XBOOLE_0:def_3;
then  x in [#] (One-Point_Compactification X) by Def9;
then consider B being set  such that
A11: x in B and
A12: B in F by A3, TARSKI:def_4;
reconsider B = B as Subset of (One-Point_Compactification X) by A12;
 B is open by A2, A12, TOPS_2:def_1;
then  B in the topology of (One-Point_Compactification X) by PRE_TOPC:def_2;
then A13: B in the topology of X \/  {  (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact )  }  by Def9;
percases ( B in the topology of X or B in  {  (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact )  }  ) by A13, XBOOLE_0:def_3;
supposeA14: B in the topology of X ; ::_thesis: x in union Fx
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, PRE_TOPC:def_2;
then  Bx in Fx by A15;
hence  x in union Fx by A11, TARSKI:def_4; ::_thesis: verum
end;
suppose B in  {  (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact )  }  ; ::_thesis: x in union Fx
then consider Bx being 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__::_thesis:_not_x_in_{([#]_X)}
assume  x in {([#] X)} ; ::_thesis: contradiction
then  x = [#] X by TARSKI:def_1;
hence  contradiction by A10; ::_thesis: verum
end;
then  x in Bx by A11, A16, XBOOLE_0:def_3;
hence  x in union Fx by A18, TARSKI:def_4; ::_thesis: verum
end;
end;
end;
then  [#] X = union Fx by SETFAM_1:45;
then  Fx is Cover of U ` by SETFAM_1:def_11;
then consider Gx being 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, COMPTS_1:def_4;
set GX =  {  W where W is Subset of (One-Point_Compactification X) : ( W in F & ex V being 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:  {  W where W is Subset of (One-Point_Compactification X) : ( W in F & ex V being 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)} ) ) ) )  }  c= the topology of (One-Point_Compactification X)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  W where W is Subset of (One-Point_Compactification X) : ( W in F & ex V being 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)} ) ) ) )  }  or x in the topology of (One-Point_Compactification X) )
assume  x in  {  W where W is Subset of (One-Point_Compactification X) : ( W in F & ex V being 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)} ) ) ) )  }  ; ::_thesis: x in the topology of (One-Point_Compactification X)
then consider W being Subset of (One-Point_Compactification X) such that
A23: x = W and
A24: W in F and
 ex V being 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, TOPS_2:def_1;
hence  x in the topology of (One-Point_Compactification X) by A23, PRE_TOPC:def_2; ::_thesis: verum
end;
defpred S1[ set , set ] means ( X in Gx & ( X \/ {([#] X)} in F implies c2 = X \/ {([#] X)} ) & ( not X \/ {([#] X)} in F implies c2 = X ) );
A25: for x being set st x in Gx holds
ex y being set st
( y in  {  W where W is Subset of (One-Point_Compactification X) : ( W in F & ex V being 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)} ) ) ) )  }  & S1[x,y] )
proof
let x be set ; ::_thesis: ( x in Gx implies ex y being set st
( y in  {  W where W is Subset of (One-Point_Compactification X) : ( W in F & ex V being 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)} ) ) ) )  }  & S1[x,y] ) )
assume A26: x in Gx ; ::_thesis: ex y being set st
( y in  {  W where W is Subset of (One-Point_Compactification X) : ( W in F & ex V being 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)} ) ) ) )  }  & S1[x,y] )
then  x in Fx by A19;
then consider U being 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 ) ;
percases ( not U \/ {([#] X)} in F or U \/ {([#] X)} in F ) ;
supposeA29: not U \/ {([#] X)} in F ; ::_thesis: ex y being set st
( y in  {  W where W is Subset of (One-Point_Compactification X) : ( W in F & ex V being 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)} ) ) ) )  }  & S1[x,y] )
then reconsider y = U as Subset of (One-Point_Compactification X) by A28;
take  y ; ::_thesis: ( y in  {  W where W is Subset of (One-Point_Compactification X) : ( W in F & ex V being 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)} ) ) ) )  }  & S1[x,y] )
thus  y in  {  W where W is Subset of (One-Point_Compactification X) : ( W in F & ex V being 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)} ) ) ) )  }  by A26, A27, A28, A29; ::_thesis: S1[x,y]
thus  S1[x,y] by A26, A27, A29; ::_thesis: verum
end;
supposeA30: U \/ {([#] X)} in F ; ::_thesis: ex y being set st
( y in  {  W where W is Subset of (One-Point_Compactification X) : ( W in F & ex V being 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)} ) ) ) )  }  & S1[x,y] )
then reconsider y = U \/ {([#] X)} as Subset of (One-Point_Compactification X) ;
take  y ; ::_thesis: ( y in  {  W where W is Subset of (One-Point_Compactification X) : ( W in F & ex V being 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)} ) ) ) )  }  & S1[x,y] )
thus  y in  {  W where W is Subset of (One-Point_Compactification X) : ( W in F & ex V being 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)} ) ) ) )  }  by A26, A27, A30; ::_thesis: S1[x,y]
thus  S1[x,y] by A26, A27, A30; ::_thesis: verum
end;
end;
end;
consider f being Function such that
A31: dom f = Gx and
 rng f c=  {  W where W is Subset of (One-Point_Compactification X) : ( W in F & ex V being 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)} ) ) ) )  }  and
A32: for x being set st x in Gx holds
S1[x,f . x] from FUNCT_1:sch_5(A25);
A33:  {  W where W is Subset of (One-Point_Compactification X) : ( W in F & ex V being 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)} ) ) ) )  }  c= rng f
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in  {  W where W is Subset of (One-Point_Compactification X) : ( W in F & ex V being 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)} ) ) ) )  }  or y in rng f )
assume  y in  {  W where W is Subset of (One-Point_Compactification X) : ( W in F & ex V being 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)} ) ) ) )  }  ; ::_thesis: y in rng f
then consider W being Subset of (One-Point_Compactification X) such that
A34: y = W and
 W in F and
A35: ex V being 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 being 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;
 f . V in rng f by A31, A36, FUNCT_1:3;
hence  y in rng f by A32, A34, A36, A37; ::_thesis: verum
end;
 rng f is finite by A21, A31, FINSET_1:8;
then reconsider GX =  {  W where W is Subset of (One-Point_Compactification X) : ( W in F & ex V being 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)} ) ) ) )  }  as finite Subset-Family of (One-Point_Compactification X) by A33, A22, XBOOLE_1:1;
take G = GX \/ {A}; ::_thesis: ( G c= F & G is Cover of the carrier of (One-Point_Compactification X) & G is finite )
A38: GX c= F
proof
let P be set ; :: according to TARSKI:def_3 ::_thesis: ( not P in GX or P in F )
assume  P in GX ; ::_thesis: P in F
then  ex W being Subset of (One-Point_Compactification X) st
( P = W & W in F & ex V being 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  P in F ; ::_thesis: verum
end;
 {A} c= F by A6, ZFMISC_1:31;
hence  G c= F by A38, XBOOLE_1:8; ::_thesis: ( G is Cover of the carrier of (One-Point_Compactification X) & G is finite )
 union G = [#] (One-Point_Compactification X)
proof
thus  union G c= [#] (One-Point_Compactification X) ; :: according to XBOOLE_0:def_10 ::_thesis: [#] (One-Point_Compactification X) c= union G
let P be set ; :: according to TARSKI:def_3 ::_thesis: ( not P in [#] (One-Point_Compactification X) or P in union G )
assume  P in [#] (One-Point_Compactification X) ; ::_thesis: P in union G
then A39: P in succ ([#] X) by Def9;
percases ( P in [#] X or P in {([#] X)} ) by A39, XBOOLE_0:def_3;
suppose P in [#] X ; ::_thesis: P in union G
then  P in (U `) \/ U by PRE_TOPC:2;
then A40: ( P in U ` or P in U ) by XBOOLE_0:def_3;
A41: union Gx c= union GX
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in union Gx or z in union GX )
assume  z in union Gx ; ::_thesis: z in union GX
then consider S being set  such that
A42: z in S and
A43: S in Gx by TARSKI:def_4;
 S in Fx by A19, A43;
then consider Z being Subset of X such that
A44: S = Z and
 Z is open and
A45: ( ( Z in F & not Z \/ {([#] X)} in F ) or Z \/ {([#] X)} in F ) ;
percases ( ( Z in F & not Z \/ {([#] X)} in F ) or Z \/ {([#] X)} in F ) by A45;
suppose ( Z in F & not Z \/ {([#] X)} in F ) ; ::_thesis: z in union GX
then  Z in GX by A43, A44;
hence  z in union GX by A42, A44, TARSKI:def_4; ::_thesis: verum
end;
supposeA46: Z \/ {([#] X)} in F ; ::_thesis: z in union GX
A47: z in Z \/ {([#] X)} by A42, A44, XBOOLE_0:def_3;
 Z \/ {([#] X)} in GX by A43, A44, A46;
hence  z in union GX by A47, TARSKI:def_4; ::_thesis: verum
end;
end;
end;
 U ` c= union Gx by A20, SETFAM_1:def_11;
then  ( P in union Gx or P in U ) by A40;
then  ( P in union GX or P in A ) by A8, A41, 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  P in union G by ZFMISC_1:78; ::_thesis: verum
end;
supposeA48: P in {([#] X)} ; ::_thesis: P in union G
 A in {A} by TARSKI:def_1;
then A49: A in G by XBOOLE_0:def_3;
 P = [#] X by A48, TARSKI:def_1;
hence  P in union G by A5, A49, TARSKI:def_4; ::_thesis: verum
end;
end;
end;
hence  G is Cover of (One-Point_Compactification X) by SETFAM_1:def_11; ::_thesis: G is finite
thus  G is finite ; ::_thesis: verum
end;
end;

theorem :: COMPACT1:6
for X being non empty TopSpace holds
( ( X is Hausdorff & X is locally-compact ) iff One-Point_Compactification X is Hausdorff )
proof
let X be non empty TopSpace; ::_thesis: ( ( X is Hausdorff & X is locally-compact ) iff One-Point_Compactification X is Hausdorff )
set D =  {  (U \/ {([#] X)}) where U is 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 \/  {  (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact )  }  by Def9;
A4: [#] X c= [#] (One-Point_Compactification X) by Th4;
thus  ( X is Hausdorff & X is locally-compact implies One-Point_Compactification X is Hausdorff ) ::_thesis: ( One-Point_Compactification X is Hausdorff implies ( X is Hausdorff & X is locally-compact ) )
proof
assume that
A5: X is Hausdorff and
A6: X is locally-compact ; ::_thesis: One-Point_Compactification X is Hausdorff
let p, q be Point of (One-Point_Compactification X); :: according to PRE_TOPC:def_10 ::_thesis: ( p = q or ex b1, b2 being Element of K19( the carrier of (One-Point_Compactification X)) st
( b1 is open & b2 is open & p in b1 & q in b2 & b1 misses b2 ) )
assume A7: p <> q ; ::_thesis: ex b1, b2 being Element of K19( the carrier of (One-Point_Compactification X)) st
( b1 is open & b2 is open & p in b1 & q in b2 & b1 misses b2 )
percases ( ( p in [#] X & q in [#] X ) or ( p in [#] X & q in {([#] X)} ) or ( q in [#] X & p in {([#] X)} ) or ( p in {([#] X)} & q in {([#] X)} ) ) by A2, XBOOLE_0:def_3;
suppose ( p in [#] X & q in [#] X ) ; ::_thesis: ex b1, b2 being Element of K19( the carrier of (One-Point_Compactification X)) st
( b1 is open & b2 is open & p in b1 & q in b2 & b1 misses b2 )
then consider W, V being 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, PRE_TOPC:def_10;
reconsider W = W, V = V as Subset of (One-Point_Compactification X) by A4, XBOOLE_1:1;
 V in the topology of X by A9, PRE_TOPC:def_2;
then A13: V in the topology of (One-Point_Compactification X) by A3, XBOOLE_0:def_3;
take  W ; ::_thesis: ex b1 being Element of K19( the carrier of (One-Point_Compactification X)) st
( W is open & b1 is open & p in W & q in b1 & W misses b1 )
take  V ; ::_thesis: ( W is open & V is open & p in W & q in V & W misses V )
 W in the topology of X by A8, PRE_TOPC:def_2;
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, PRE_TOPC:def_2; ::_thesis: ( p in W & q in V & W misses V )
thus  ( p in W & q in V & W misses V ) by A10, A11, A12; ::_thesis: verum
end;
supposethat A14: p in [#] X and
A15: q in {([#] X)} ; ::_thesis: ex b1, b2 being Element of K19( the carrier of (One-Point_Compactification X)) st
( b1 is open & b2 is open & p in b1 & q in b2 & b1 misses b2 )
reconsider px = p as Point of X by A14;
consider P being a_neighborhood of px such that
A16: P is compact by A6, Def6;
 [#] 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  {  (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact )  }  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 ; ::_thesis: ex b1 being Element of K19( the carrier of (One-Point_Compactification X)) st
( W is open & b1 is open & p in W & q in b1 & W misses b1 )
take  V ; ::_thesis: ( W is open & V is open & p in W & q in V & W misses 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 by PRE_TOPC:def_2; ::_thesis: ( V is open & p in W & q in V & W misses V )
thus  V is open by A17, PRE_TOPC:def_2; ::_thesis: ( p in W & q in V & W misses V )
thus  p in W by CONNSP_2:def_1; ::_thesis: ( q in V & W misses V )
thus  q in V by A15, XBOOLE_0:def_3; ::_thesis: W misses V
 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  W misses V by A18, XBOOLE_1:70; ::_thesis: verum
end;
supposethat A19: q in [#] X and
A20: p in {([#] X)} ; ::_thesis: ex b1, b2 being Element of K19( the carrier of (One-Point_Compactification X)) st
( b1 is open & b2 is open & p in b1 & q in b2 & b1 misses b2 )
reconsider qx = q as Point of X by A19;
consider Q being a_neighborhood of qx such that
A21: Q is compact by A6, Def6;
 [#] 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  {  (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact )  }  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 ; ::_thesis: ex b1 being Element of K19( the carrier of (One-Point_Compactification X)) st
( V is open & b1 is open & p in V & q in b1 & V misses b1 )
take  W ; ::_thesis: ( V is open & W is open & p in V & q in W & V misses W )
thus  V is open by A22, PRE_TOPC:def_2; ::_thesis: ( W is open & p in V & q in W & V misses W )
 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 by PRE_TOPC:def_2; ::_thesis: ( p in V & q in W & V misses W )
thus  p in V by A20, XBOOLE_0:def_3; ::_thesis: ( q in W & V misses W )
thus  q in W by CONNSP_2:def_1; ::_thesis: V misses W
 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  V misses W by A23, XBOOLE_1:70; ::_thesis: verum
end;
supposeA24: ( p in {([#] X)} & q in {([#] X)} ) ; ::_thesis: ex b1, b2 being Element of K19( the carrier of (One-Point_Compactification X)) st
( b1 is open & b2 is open & p in b1 & q in b2 & b1 misses b2 )
then  p = [#] X by TARSKI:def_1;
hence  ex b1, b2 being Element of K19( the carrier of (One-Point_Compactification X)) st
( b1 is open & b2 is open & p in b1 & q in b2 & b1 misses b2 ) by A7, A24, TARSKI:def_1; ::_thesis: verum
end;
end;
end;
A25: X is SubSpace of One-Point_Compactification X by Th5;
assume A26: One-Point_Compactification X is Hausdorff ; ::_thesis: ( X is Hausdorff & X is locally-compact )
hence  X is Hausdorff by A25; ::_thesis: X is locally-compact
let x be Point of X; :: according to COMPACT1:def_6 ::_thesis: ex U being a_neighborhood of x st U is compact
 x in [#] X ;
then reconsider p = x as Point of (One-Point_Compactification X) by A4;
 not [#] X in [#] X ;
then  p <> q ;
then consider V, U being 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, PRE_TOPC:def_10;
A32: now__::_thesis:_not_U_in_the_topology_of_X
assume  U in the topology of X ; ::_thesis: contradiction
then  q in [#] X by A30;
hence  contradiction ; ::_thesis: verum
end;
 U in the topology of (One-Point_Compactification X) by A28, PRE_TOPC:def_2;
then  U in  {  (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact )  }  by A3, A32, XBOOLE_0:def_3;
then consider W being 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__::_thesis:_not_V_in__{__(U_\/_{([#]_X)})_where_U_is_Subset_of_X_:_(_U_is_open_&_U_`_is_compact_)__}_
assume  V in  {  (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact )  }  ; ::_thesis: contradiction
then  ex S being 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 ; ::_thesis: verum
end;
 V in the topology of (One-Point_Compactification X) by A27, PRE_TOPC:def_2;
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 (Cl Vx) by PRE_TOPC:18, TOPS_1:19;
 x in Int Vx by A29, TOPS_1:23;
then reconsider K = Cl Vx as a_neighborhood of x by A42, CONNSP_2:def_1;
take  K ; ::_thesis: K is compact
 (U `) /\ ([#] X) = W ` by A38, XBOOLE_1:28;
then  W ` is closed by A25, A28, PRE_TOPC:13;
hence  K is compact by A34, A39, A38, COMPTS_1:9, TOPS_1:5; ::_thesis: verum
end;

theorem Th7: :: COMPACT1:7
for X being non empty TopSpace holds
( not X is compact iff ex X9 being Subset of (One-Point_Compactification X) st
( X9 = [#] X & X9 is dense ) )
proof
let X be non empty TopSpace; ::_thesis: ( not X is compact iff ex X9 being Subset of (One-Point_Compactification X) st
( X9 = [#] X & X9 is dense ) )
set D =  {  (U \/ {([#] X)}) where U is 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 \/  {  (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact )  }  by Def9;
thus  ( not X is compact implies ex X9 being Subset of (One-Point_Compactification X) st
( X9 = [#] X & X9 is dense ) ) ::_thesis: ( ex X9 being Subset of (One-Point_Compactification X) st
( X9 = [#] X & X9 is dense ) implies not X is compact )
proof
assume  not X is compact ; ::_thesis: ex X9 being Subset of (One-Point_Compactification X) st
( X9 = [#] X & X9 is dense )
then A6: not [#] X is compact by COMPTS_1:1;
 [#] X c= [#] (One-Point_Compactification X) by Th4;
then reconsider X9 = [#] X as Subset of (One-Point_Compactification X) ;
take  X9 ; ::_thesis: ( X9 = [#] X & X9 is dense )
thus  X9 = [#] X ; ::_thesis: X9 is dense
thus  Cl X9 c= [#] (One-Point_Compactification X) ; :: according to XBOOLE_0:def_10,TOPS_1:def_3 ::_thesis: [#] (One-Point_Compactification X) c= Cl X9
A7: [#] X c= Cl X9 by PRE_TOPC:18;
A8: now__::_thesis:_[#]_X_in_Cl_X9
reconsider Xe = [#] X as Element of (One-Point_Compactification X) by A3, A2, XBOOLE_0:def_3;
assume A9: not [#] X in Cl X9 ; ::_thesis: contradiction
reconsider XX = {Xe} as Subset of (One-Point_Compactification X) ;
A10: now__::_thesis:_not_XX_in_the_topology_of_X
assume  XX in the topology of X ; ::_thesis: contradiction
then  [#] X in [#] X by A3;
hence  contradiction ; ::_thesis: verum
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) by PRE_TOPC:def_2;
then  XX in  {  (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact )  }  by A5, A10, XBOOLE_0:def_3;
then consider U being Subset of X such that
A11: XX = U \/ {([#] X)} and
 U is open and
A12: U ` is compact ;
now__::_thesis:_not_U_=_XX
assume  U = XX ; ::_thesis: contradiction
then  [#] X in [#] X by A3;
hence  contradiction ; ::_thesis: verum
end;
then  U = {} X by A11, ZFMISC_1:37;
hence  contradiction by A6, A12; ::_thesis: verum
end;
 [#] (One-Point_Compactification X) c= (Cl X9) \/ {([#] X)} by A2, PRE_TOPC:18, XBOOLE_1:9;
hence  [#] (One-Point_Compactification X) c= Cl X9 by A8, ZFMISC_1:40; ::_thesis: verum
end;
given X9 being Subset of (One-Point_Compactification X) such that A13: X9 = [#] X and
A14: X9 is dense ; ::_thesis: not X is compact
A15: Cl X9 = [#] (One-Point_Compactification X) by A14, TOPS_1:def_3;
assume  X is compact ; ::_thesis: contradiction
then  [#] X is compact ;
then  ({} X) ` is compact ;
then  ({} X) \/ {([#] X)} in  {  (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact )  }  ;
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, PRE_TOPC:def_2;
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; ::_thesis: verum
end;

theorem :: COMPACT1:8
for X being non empty TopSpace st not X is compact holds
incl (X,(One-Point_Compactification X)) is compactification
proof
let X be non empty TopSpace; ::_thesis: ( not X is compact implies incl (X,(One-Point_Compactification X)) is compactification )
set h = incl (X,(One-Point_Compactification X));
set D =  {  (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact )  }  ;
assume  not X is compact ; ::_thesis: incl (X,(One-Point_Compactification X)) is compactification
then A1: ex X9 being 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 \/  {  (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact )  }  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 :: according to XBOOLE_0:def_10 ::_thesis: the topology of X c= the topology of ((One-Point_Compactification X) | Xy)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the topology of ((One-Point_Compactification X) | Xy) or x in the topology of X )
assume A5: x in the topology of ((One-Point_Compactification X) | Xy) ; ::_thesis: x in the topology of X
then reconsider P = x as Subset of ((One-Point_Compactification X) | Xy) ;
consider Q being 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;
percases ( Q in the topology of X or Q in  {  (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact )  }  ) by A4, A6, XBOOLE_0:def_3;
suppose Q in the topology of X ; ::_thesis: x in the topology of X
hence  x in the topology of X by A3, A7, XBOOLE_1:28; ::_thesis: verum
end;
suppose Q in  {  (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact )  }  ; ::_thesis: x in the topology of X
then consider U being 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) = {} by XBOOLE_0:def_7;
then P = (U /\ ([#] X)) \/ {} by A3, A7, A8, XBOOLE_1:23
.= U by XBOOLE_1:28 ;
hence  x in the topology of X by A9, PRE_TOPC:def_2; ::_thesis: verum
end;
end;
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the topology of X or x in the topology of ((One-Point_Compactification X) | Xy) )
assume A10: x in the topology of X ; ::_thesis: x in the topology of ((One-Point_Compactification X) | Xy)
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  x in the topology of ((One-Point_Compactification X) | Xy) by A11, PRE_TOPC:def_4; ::_thesis: verum
end;
hence  incl (X,(One-Point_Compactification X)) is embedding by A2, Th3; :: according to COMPACT1:def_8 ::_thesis: ( One-Point_Compactification X is compact & (incl (X,(One-Point_Compactification X))) .: ([#] X) is dense )
thus  One-Point_Compactification X is compact ; ::_thesis: (incl (X,(One-Point_Compactification X))) .: ([#] X) is dense
thus  (incl (X,(One-Point_Compactification X))) .: ([#] X) is dense by A2, A1, Th2; ::_thesis: verum
end;