let X be non empty TopSpace; :: thesis: ( not X is compact iff ex X' being Subset of (One-Point_Compactification X) st
( X' = [#] X & X' is dense ) )
set D = { (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact ) } ;
A1: 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;
A2: [#] X in {([#] X)} by TARSKI:def 1;
A3: [#] (One-Point_Compactification X) = succ ([#] X) by Def9;
thus ( not X is compact implies ex X' being Subset of (One-Point_Compactification X) st
( X' = [#] X & X' is dense ) ) :: thesis: ( ex X' being Subset of (One-Point_Compactification X) st
( X' = [#] X & X' is dense ) implies not X is compact )

proof

assume not X is compact ; :: thesis: ex X' being Subset of (One-Point_Compactification X) st
( X' = [#] X & X' is dense )
then A4: not [#] X is compact by COMPTS_1:10;
[#] X c= [#] (One-Point_Compactification X) by Th4;
then reconsider X' = [#] X as Subset of (One-Point_Compactification X) ;
take X' ; :: thesis: ( X' = [#] X & X' is dense )
thus X' = [#] X ; :: thesis: X' is dense
thus Cl X' c= [#] (One-Point_Compactification X) ; :: according to XBOOLE_0:def 10,TOPS_1:def 3 :: thesis: [#] (One-Point_Compactification X) c= Cl X'
A5: [#] X c= Cl X' by PRE_TOPC:48;
A6: [#] (One-Point_Compactification X) c= (Cl X') \/ {([#] X)} by A3, PRE_TOPC:48, XBOOLE_1:9;

now

assume A7: not [#] X in Cl X' ; :: thesis: contradiction
reconsider Xe = [#] X as Element of (One-Point_Compactification X) by A2, A3, XBOOLE_0:def 3;
reconsider XX = {Xe} as Subset of (One-Point_Compactification X) ;
([#] (One-Point_Compactification X)) \ (Cl X') = (([#] X) \ (Cl X')) \/ ({([#] X)} \ (Cl X')) by A3, XBOOLE_1:42
.= {} \/ ({([#] X)} \ (Cl X')) by A5, XBOOLE_1:37
.= XX by A7, ZFMISC_1:67 ;
then A8: XX is open by PRE_TOPC:def 6;

A9: now

assume XX in the topology of X ; :: thesis: contradiction
then [#] X in [#] X by A2;
hence contradiction ; :: thesis: verum

end;

XX in the topology of (One-Point_Compactification X) by A8, PRE_TOPC:def 5;
then XX in { (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact ) } by A1, A9, XBOOLE_0:def 3;
then consider U being Subset of X such that
A10: XX = U \/ {([#] X)} and
U is open and
A11: U ` is compact ;

now

assume U = XX ; :: thesis: contradiction
then [#] X in [#] X by A2;
hence contradiction ; :: thesis: verum

end;

then U = {} X by A10, ZFMISC_1:43;
hence contradiction by A4, A11; :: thesis: verum

end;

hence [#] (One-Point_Compactification X) c= Cl X' by A6, ZFMISC_1:46; :: thesis: verum

end;

given X' being Subset of (One-Point_Compactification X) such that A12: X' = [#] X and
A13: X' is dense ; :: thesis: not X is compact
A14: Cl X' = [#] (One-Point_Compactification X) by A13, 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 A15: {([#] X)} in the topology of (One-Point_Compactification X) by A1, XBOOLE_0:def 3;
then reconsider X1 = {([#] X)} as Subset of (One-Point_Compactification X) ;
X1 is open by A15, PRE_TOPC:def 5;
then A16: Cl (X1 ` ) = X1 ` by PRE_TOPC:52;
A17: not [#] X in [#] X ;
A18: X1 ` = ([#] X) \ X1 by A3, XBOOLE_1:40
.= [#] X by A17, ZFMISC_1:65 ;
[#] X in [#] (One-Point_Compactification X) by A2, A3, XBOOLE_0:def 3;
hence contradiction by A12, A14, A16, A18; :: thesis: verum