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 ) )

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

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;

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;

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

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

A25:
X is SubSpace of One-Point_Compactification X
by Th5;
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 b_{1}, b_{2} being Element of K19( the carrier of (One-Point_Compactification X)) st

( b_{1} is open & b_{2} is open & p in b_{1} & q in b_{2} & b_{1} misses b_{2} ) )

assume A7: p <> q ; :: thesis: ex b_{1}, b_{2} being Element of K19( the carrier of (One-Point_Compactification X)) st

( b_{1} is open & b_{2} is open & p in b_{1} & q in b_{2} & b_{1} misses b_{2} )

end;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 b

( b

assume A7: p <> q ; :: thesis: ex b

( b

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 A2, XBOOLE_0:def 3;

end;

suppose
( p in [#] X & q in [#] X )
; :: thesis: ex b_{1}, b_{2} being Element of K19( the carrier of (One-Point_Compactification X)) st

( b_{1} is open & b_{2} is open & p in b_{1} & q in b_{2} & b_{1} misses b_{2} )

( b

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 (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 ; :: thesis: ex b_{1} being Element of K19( the carrier of (One-Point_Compactification X)) st

( W is open & b_{1} is open & p in W & q in b_{1} & W misses b_{1} )

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 (One-Point_Compactification X) by A3, XBOOLE_0:def 3;

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 A10, A11, A12; :: thesis: verum

end;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 (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 ; :: thesis: ex b

( W is open & b

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 (One-Point_Compactification X) by A3, XBOOLE_0:def 3;

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 A10, A11, A12; :: thesis: verum

suppose that A14:
p in [#] X
and

A15: q in {([#] X)} ; :: thesis: ex b_{1}, b_{2} being Element of K19( the carrier of (One-Point_Compactification X)) st

( b_{1} is open & b_{2} is open & p in b_{1} & q in b_{2} & b_{1} misses b_{2} )

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

( b

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= [#] (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 b_{1} being Element of K19( the carrier of (One-Point_Compactification X)) st

( W is open & b_{1} is open & p in W & q in b_{1} & W misses b_{1} )

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 ; :: 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 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;consider P being 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 { (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 b

( W is open & b

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 ; :: 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 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

suppose that A19:
q in [#] X
and

A20: p in {([#] X)} ; :: thesis: ex b_{1}, b_{2} being Element of K19( the carrier of (One-Point_Compactification X)) st

( b_{1} is open & b_{2} is open & p in b_{1} & q in b_{2} & b_{1} misses b_{2} )

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

( b

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= [#] (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 b_{1} being Element of K19( the carrier of (One-Point_Compactification X)) st

( V is open & b_{1} is open & p in V & q in b_{1} & V misses b_{1} )

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 (One-Point_Compactification X) by A3, XBOOLE_0:def 3;

hence W is open ; :: 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;consider Q being 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 { (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 b

( V is open & b

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 (One-Point_Compactification X) by A3, XBOOLE_0:def 3;

hence W is open ; :: 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

suppose A24:
( p in {([#] X)} & q in {([#] X)} )
; :: thesis: ex b_{1}, b_{2} being Element of K19( the carrier of (One-Point_Compactification X)) st

( b_{1} is open & b_{2} is open & p in b_{1} & q in b_{2} & b_{1} misses b_{2} )

( b

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

hence ex b_{1}, b_{2} being Element of K19( the carrier of (One-Point_Compactification X)) st

( b_{1} is open & b_{2} is open & p in b_{1} & q in b_{2} & b_{1} misses b_{2} )
by A7, A24, TARSKI:def 1; :: thesis: verum

end;hence ex b

( b

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

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;

A32: now :: thesis: not U in the topology of X

U in the topology of (One-Point_Compactification X)
by A28;assume
U in the topology of X
; :: thesis: contradiction

then q in [#] X by A30;

hence contradiction ; :: thesis: verum

end;then q in [#] X by A30;

hence contradiction ; :: thesis: verum

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 ) }

V in the topology of (One-Point_Compactification X)
by A27;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;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

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