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: [#] = succ ([#] X) by Def9;
[#] X in {([#] X)} by TARSKI:def 1;
then reconsider q = [#] X as Point of by ;
A3: the topology of = the topology of X \/ { (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact ) } by Def9;
A4: [#] X c= [#] 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:
let p, q be Point of ; :: according to PRE_TOPC:def 10 :: thesis: ( p = q or ex b1, b2 being Element of K19( the carrier of ) 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 ) st
( b1 is open & b2 is open & p in b1 & q in b2 & b1 misses b2 )

per cases ( ( 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 ;
suppose ( p in [#] X & q in [#] X ) ; :: thesis: ex b1, b2 being Element of K19( the carrier of ) 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;
reconsider W = W, V = V as Subset of by ;
V in the topology of X by A9;
then A13: V in the topology of by ;
take W ; :: thesis: ex b1 being Element of K19( the carrier of ) 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;
then W in the topology of by ;
hence ( W is open & V is open ) by A13; :: thesis: ( p in W & q in V & W misses V )
thus ( p in W & q in V & W misses V ) by ; :: thesis: verum
end;
suppose that A14: p in [#] X and
A15: q in {([#] X)} ; :: thesis: ex b1, b2 being Element of K19( the carrier of ) 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;
[#] X c= [#] by ;
then reconsider W = Int P as Subset of 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 ;
then A17: (P `) \/ {([#] X)} in the topology of by ;
then reconsider V = (P `) \/ {([#] X)} as Subset of ;
take W ; :: thesis: ex b1 being Element of K19( the carrier of ) 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 by ;
hence W is open ; :: thesis: ( V is open & p in W & q in V & W misses V )
thus V is open by A17; :: 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 ; :: 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 ; :: thesis: verum
end;
suppose that A19: q in [#] X and
A20: p in {([#] X)} ; :: thesis: ex b1, b2 being Element of K19( the carrier of ) 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;
[#] X c= [#] by Th4;
then reconsider W = Int Q as Subset of 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 ;
then A22: (Q `) \/ {([#] X)} in the topology of by ;
then reconsider V = (Q `) \/ {([#] X)} as Subset of ;
take V ; :: thesis: ex b1 being Element of K19( the carrier of ) 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; :: 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 by ;
hence W is open ; :: thesis: ( p in V & q in W & V misses W )
thus p in V by ; :: 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 ; :: thesis: verum
end;
suppose A24: ( p in {([#] X)} & q in {([#] X)} ) ; :: thesis: ex b1, b2 being Element of K19( the carrier of ) 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 ) st
( b1 is open & b2 is open & p in b1 & q in b2 & b1 misses b2 ) by ; :: 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:
let x be Point of X; :: according to COMPACT1:def 6 :: thesis: ex U being a_neighborhood of x st U is compact
reconsider p = x as Point of by A4;
not [#] X in [#] X ;
then p <> q ;
then consider V, U being Subset of 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 :: 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 by A28;
then U in { (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact ) } by ;
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
.= (([#] X) \ W) /\ ([#] X) by
.= ([#] X) \ W by XBOOLE_1:28 ;
A36: [#] X in {([#] X)} by TARSKI:def 1;
then A37: [#] X in U by ;
A38: \ U = (([#] X) \ U) \/ ({([#] X)} \ U) by
.= (([#] X) \ W) \/ {} by
.= W ` ;
A39: V c= U ` by ;
then A40: V c= [#] X by ;
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 ;
then [#] X in [#] X by A40;
hence contradiction ; :: thesis: verum
end;
V in the topology of by A27;
then V in the topology of X by ;
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 ;
x in Int Vx by ;
then reconsider K = Cl Vx as a_neighborhood of x by ;
take K ; :: thesis: K is compact
(U `) /\ ([#] X) = W ` by ;
then W ` is closed by ;
hence K is compact by ; :: thesis: verum