let X be non empty TopSpace; :: thesis: ( not X is compact iff ex X9 being Subset of (One-Point_Compactification X) st

( X9 = [#] X & X9 is dense ) )

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;

A3: [#] X in {([#] X)} by TARSKI:def 1;

then A4: [#] X in [#] (One-Point_Compactification X) by A2, XBOOLE_0:def 3;

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

thus ( not X is compact implies ex X9 being Subset of (One-Point_Compactification X) st

( X9 = [#] X & X9 is dense ) ) :: thesis: ( ex X9 being Subset of (One-Point_Compactification X) st

( X9 = [#] X & X9 is dense ) implies not X is compact )

A14: X9 is dense ; :: thesis: not X is compact

A15: Cl X9 = [#] (One-Point_Compactification X) by A14;

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 A16: {([#] X)} in the topology of (One-Point_Compactification X) by A5, XBOOLE_0:def 3;

then reconsider X1 = {([#] X)} as Subset of (One-Point_Compactification X) ;

X1 is open by A16;

then A17: Cl (X1 `) = X1 ` by PRE_TOPC:22;

X1 ` = ([#] X) \ X1 by A2, XBOOLE_1:40

.= [#] X by A1, ZFMISC_1:57 ;

hence contradiction by A13, A15, A17, A4; :: thesis: verum

( X9 = [#] X & X9 is dense ) )

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;

A3: [#] X in {([#] X)} by TARSKI:def 1;

then A4: [#] X in [#] (One-Point_Compactification X) by A2, XBOOLE_0:def 3;

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

thus ( not X is compact implies ex X9 being Subset of (One-Point_Compactification X) st

( X9 = [#] X & X9 is dense ) ) :: thesis: ( ex X9 being Subset of (One-Point_Compactification X) st

( X9 = [#] X & X9 is dense ) implies not X is compact )

proof

given X9 being Subset of (One-Point_Compactification X) such that A13:
X9 = [#] X
and
assume
not X is compact
; :: thesis: ex X9 being Subset of (One-Point_Compactification X) st

( X9 = [#] X & X9 is dense )

then A6: not [#] X is compact ;

[#] X c= [#] (One-Point_Compactification X) by Th4;

then reconsider X9 = [#] X as Subset of (One-Point_Compactification X) ;

take X9 ; :: thesis: ( X9 = [#] X & X9 is dense )

thus X9 = [#] X ; :: thesis: X9 is dense

thus Cl X9 c= [#] (One-Point_Compactification X) ; :: according to XBOOLE_0:def 10,TOPS_1:def 3 :: thesis: [#] (One-Point_Compactification X) c= Cl X9

A7: [#] X c= Cl X9 by PRE_TOPC:18;

hence [#] (One-Point_Compactification X) c= Cl X9 by A8, ZFMISC_1:40; :: thesis: verum

end;( X9 = [#] X & X9 is dense )

then A6: not [#] X is compact ;

[#] X c= [#] (One-Point_Compactification X) by Th4;

then reconsider X9 = [#] X as Subset of (One-Point_Compactification X) ;

take X9 ; :: thesis: ( X9 = [#] X & X9 is dense )

thus X9 = [#] X ; :: thesis: X9 is dense

thus Cl X9 c= [#] (One-Point_Compactification X) ; :: according to XBOOLE_0:def 10,TOPS_1:def 3 :: thesis: [#] (One-Point_Compactification X) c= Cl X9

A7: [#] X c= Cl X9 by PRE_TOPC:18;

A8: now :: thesis: [#] X in Cl X9

[#] (One-Point_Compactification X) c= (Cl X9) \/ {([#] X)}
by A2, PRE_TOPC:18, XBOOLE_1:9;reconsider Xe = [#] X as Element of (One-Point_Compactification X) by A3, A2, XBOOLE_0:def 3;

assume A9: not [#] X in Cl X9 ; :: thesis: contradiction

reconsider XX = {Xe} as Subset of (One-Point_Compactification X) ;

.= {} \/ ({([#] X)} \ (Cl X9)) by A7, XBOOLE_1:37

.= XX by A9, ZFMISC_1:59 ;

then XX is open by PRE_TOPC:def 3;

then XX in the topology of (One-Point_Compactification X) ;

then XX in { (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact ) } by A5, A10, XBOOLE_0:def 3;

then consider U being Subset of X such that

A11: XX = U \/ {([#] X)} and

U is open and

A12: U ` is compact ;

hence contradiction by A6, A12; :: thesis: verum

end;assume A9: not [#] X in Cl X9 ; :: thesis: contradiction

reconsider XX = {Xe} as Subset of (One-Point_Compactification X) ;

A10: now :: thesis: not XX in the topology of X

([#] (One-Point_Compactification X)) \ (Cl X9) =
(([#] X) \ (Cl X9)) \/ ({([#] X)} \ (Cl X9))
by A2, XBOOLE_1:42
assume
XX in the topology of X
; :: thesis: contradiction

then [#] X in [#] X by A3;

hence contradiction ; :: thesis: verum

end;then [#] X in [#] X by A3;

hence contradiction ; :: thesis: verum

.= {} \/ ({([#] X)} \ (Cl X9)) by A7, XBOOLE_1:37

.= XX by A9, ZFMISC_1:59 ;

then XX is open by PRE_TOPC:def 3;

then XX in the topology of (One-Point_Compactification X) ;

then XX in { (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact ) } by A5, A10, XBOOLE_0:def 3;

then consider U being Subset of X such that

A11: XX = U \/ {([#] X)} and

U is open and

A12: U ` is compact ;

now :: thesis: not U = XX

then
U = {} X
by A11, ZFMISC_1:37;assume
U = XX
; :: thesis: contradiction

then [#] X in [#] X by A3;

hence contradiction ; :: thesis: verum

end;then [#] X in [#] X by A3;

hence contradiction ; :: thesis: verum

hence contradiction by A6, A12; :: thesis: verum

hence [#] (One-Point_Compactification X) c= Cl X9 by A8, ZFMISC_1:40; :: thesis: verum

A14: X9 is dense ; :: thesis: not X is compact

A15: Cl X9 = [#] (One-Point_Compactification X) by A14;

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 A16: {([#] X)} in the topology of (One-Point_Compactification X) by A5, XBOOLE_0:def 3;

then reconsider X1 = {([#] X)} as Subset of (One-Point_Compactification X) ;

X1 is open by A16;

then A17: Cl (X1 `) = X1 ` by PRE_TOPC:22;

X1 ` = ([#] X) \ X1 by A2, XBOOLE_1:40

.= [#] X by A1, ZFMISC_1:57 ;

hence contradiction by A13, A15, A17, A4; :: thesis: verum