let X be non empty TopSpace; :: thesis:
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 T_2 & X is locally-compact implies One-Point_Compactification X is T_2 ) :: thesis:

assume that
A5: X is T_2 and
A6: X is locally-compact ; :: thesis:
let p, q be Point of (One-Point_Compactification X); :: according to PRE_TOPC:def 16 :: thesis:
assume A7: p <> q ; :: thesis:

per cases by A2, XBOOLE_0:def 3;

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

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 16;
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 5;
then A13: V in the topology of (One-Point_Compactification X) by A3, XBOOLE_0:def 3;
take W ; :: thesis:
take V ; :: thesis:
W in the topology of X by A8, PRE_TOPC:def 5;
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 5; :: thesis:
thus ( p in W & q in V & W misses V ) by A10, A11, A12; :: thesis:

end;

suppose that A14: p in [#] X and
A15: q in {([#] X)} ; :: thesis:

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:
take V ; :: thesis:
W in the topology of X by PRE_TOPC:def 5;
then W in the topology of (One-Point_Compactification X) by A3, XBOOLE_0:def 3;
hence W is open by PRE_TOPC:def 5; :: thesis:
thus V is open by A17, PRE_TOPC:def 5; :: thesis:
thus p in W by CONNSP_2:def 1; :: thesis:
thus q in V by A15, XBOOLE_0:def 3; :: thesis:
not [#] X in [#] X ;
then not [#] X in Int P ;
then A18: Int P misses {([#] X)} by ZFMISC_1:56;
Int P c= P by TOPS_1:44;
then Int P misses P ` by SUBSET_1:44;
hence W misses V by A18, XBOOLE_1:70; :: thesis:

end;

suppose that A19: q in [#] X and
A20: p in {([#] X)} ; :: thesis:

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:
take W ; :: thesis:
thus V is open by A22, PRE_TOPC:def 5; :: thesis:
W in the topology of X by PRE_TOPC:def 5;
then W in the topology of (One-Point_Compactification X) by A3, XBOOLE_0:def 3;
hence W is open by PRE_TOPC:def 5; :: thesis:
thus p in V by A20, XBOOLE_0:def 3; :: thesis:
thus q in W by CONNSP_2:def 1; :: thesis:
not [#] X in [#] X ;
then not [#] X in Int Q ;
then A23: Int Q misses {([#] X)} by ZFMISC_1:56;
Int Q c= Q by TOPS_1:44;
then Int Q misses Q ` by SUBSET_1:44;
hence V misses W by A23, XBOOLE_1:70; :: thesis:

end;

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

then p = [#] X by TARSKI:def 1;
hence ex b₁, b₂ being Element of bool the carrier of (One-Point_Compactification X) st
( b₁ is open & b₂ is open & p in b₁ & q in b₂ & b₁ misses b₂ ) by A7, A24, TARSKI:def 1; :: thesis:

end;

end;

end;

A25: X is SubSpace of One-Point_Compactification X by Th5;
assume A26: One-Point_Compactification X is T_2 ; :: thesis:
hence X is T_2 by A25; :: thesis:
let x be Point of X; :: according to COMPACT1:def 6 :: thesis:
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 16;

A32: now

assume U in the topology of X ; :: thesis:
then q in [#] X by A30;
hence contradiction ; :: thesis:

end;

U in the topology of (One-Point_Compactification X) by A28, PRE_TOPC:def 5;
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:65
.= ([#] 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:68
.= W ` ;
A39: V c= U ` by A31, SUBSET_1:43;
then A40: V c= [#] X by A38, XBOOLE_1:1;

A41: now

assume V in { (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact ) } ; :: thesis:
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:

end;

V in the topology of (One-Point_Compactification X) by A27, PRE_TOPC:def 5;
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 5;
set K = Cl Vx;
A42: Int Vx c= Int (Cl Vx) by PRE_TOPC:48, TOPS_1:48;
x in Int Vx by A29, TOPS_1:55;
then reconsider K = Cl Vx as a_neighborhood of x by A42, CONNSP_2:def 1;
take K ; :: thesis:
(U ` ) /\ ([#] X) = W ` by A38, XBOOLE_1:28;
then W ` is closed by A25, A28, PRE_TOPC:43;
hence K is compact by A34, A39, A38, COMPTS_1:18, TOPS_1:31; :: thesis: