assume that
A4: X is T_2 and
A5: X is locally-compact ; :: thesis:
let p, q be Point of (One-Point_Compactification X); :: according to PRE_TOPC:def 16 :: thesis:
assume A6: 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
A7: ( W is open & V is open ) and
A8: ( p in W & q in V & W misses V ) by A4, A6, PRE_TOPC:def 16;
reconsider W = W, V = V as Subset of (One-Point_Compactification X) by A3, XBOOLE_1:1;
take W ; :: thesis:
take V ; :: thesis:
( W in the topology of X & V in the topology of X ) by A7, PRE_TOPC:def 5;
then ( W in the topology of (One-Point_Compactification X) & V in the topology of (One-Point_Compactification X) ) by A1, XBOOLE_0:def 3;
hence ( W is open & V is open ) by PRE_TOPC:def 5; :: thesis:
thus ( p in W & q in V & W misses V ) by A8; :: thesis:

end;

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

reconsider px = p as Point of X by A9;
consider P being a_neighborhood of px such that
A11: P is compact by A5, 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;
A12: (P ` ) ` = P ;
(P ` ) \/ {([#] X)} in { (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact ) } by A11, A12, A4;
then A13: (P ` ) \/ {([#] X)} in the topology of (One-Point_Compactification X) by A1, 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 A1, XBOOLE_0:def 3;
hence W is open by PRE_TOPC:def 5; :: thesis:
thus V is open by A13, PRE_TOPC:def 5; :: thesis:
thus p in W by CONNSP_2:def 1; :: thesis:
thus q in V by A10, XBOOLE_0:def 3; :: thesis:
( Int P c= [#] X & not [#] X in [#] X ) ;
then not [#] X in Int P ;
then A14: 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 A14, XBOOLE_1:70; :: thesis:

end;

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

reconsider qx = q as Point of X by A15;
consider Q being a_neighborhood of qx such that
A17: Q is compact by A5, 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;
A18: (Q ` ) ` = Q ;
(Q ` ) \/ {([#] X)} in { (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact ) } by A17, A18, A4;
then A19: (Q ` ) \/ {([#] X)} in the topology of (One-Point_Compactification X) by A1, 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 A19, 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 A1, XBOOLE_0:def 3;
hence W is open by PRE_TOPC:def 5; :: thesis:
thus p in V by A16, XBOOLE_0:def 3; :: thesis:
thus q in W by CONNSP_2:def 1; :: thesis:
( Int Q c= [#] X & not [#] X in [#] X ) ;
then not [#] X in Int Q ;
then A20: 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 A20, XBOOLE_1:70; :: thesis:

end;

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

then ( p = [#] X & q = [#] 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 A6; :: thesis:

end;