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 )
proof
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;
A8: now :: thesis: [#] X in Cl X9
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) ;
A10: now :: thesis: not XX in the topology of X
assume XX in the topology of X ; :: thesis: contradiction
then [#] X in [#] X by A3;
hence contradiction ; :: thesis: verum
end;
([#] (One-Point_Compactification X)) \ (Cl X9) = (([#] X) \ (Cl X9)) \/ ({([#] X)} \ (Cl X9)) by A2, XBOOLE_1:42
.= {} \/ ({([#] 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
assume U = XX ; :: thesis: contradiction
then [#] X in [#] X by A3;
hence contradiction ; :: thesis: verum
end;
then U = {} X by A11, ZFMISC_1:37;
hence contradiction by A6, A12; :: thesis: verum
end;
[#] (One-Point_Compactification X) c= (Cl X9) \/ {([#] X)} by A2, PRE_TOPC:18, XBOOLE_1:9;
hence [#] (One-Point_Compactification X) c= Cl X9 by A8, ZFMISC_1:40; :: thesis: verum
end;
given X9 being Subset of (One-Point_Compactification X) such that A13: X9 = [#] X and
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