let X be non empty TopSpace; :: thesis: ( not X is compact iff ex X9 being Subset of 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: [#] = succ ([#] X) by Def9;
A3: [#] X in {([#] X)} by TARSKI:def 1;
then A4: [#] X in [#] by ;
A5: the topology of = 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 st
( X9 = [#] X & X9 is dense ) ) :: thesis: ( ex X9 being Subset of st
( X9 = [#] X & X9 is dense ) implies not X is compact )
proof
assume not X is compact ; :: thesis: ex X9 being Subset of st
( X9 = [#] X & X9 is dense )

then A6: not [#] X is compact ;
[#] X c= [#] by Th4;
then reconsider X9 = [#] X as Subset of ;
take X9 ; :: thesis: ( X9 = [#] X & X9 is dense )
thus X9 = [#] X ; :: thesis: X9 is dense
thus Cl X9 c= [#] ; :: according to XBOOLE_0:def 10,TOPS_1:def 3 :: thesis:
A7: [#] X c= Cl X9 by PRE_TOPC:18;
A8: now :: thesis: [#] X in Cl X9
reconsider Xe = [#] X as Element of by ;
assume A9: not [#] X in Cl X9 ; :: thesis: contradiction
reconsider XX = {Xe} as Subset of ;
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;
\ (Cl X9) = (([#] X) \ (Cl X9)) \/ ({([#] X)} \ (Cl X9)) by
.= {} \/ ({([#] X)} \ (Cl X9)) by
.= XX by ;
then XX is open by PRE_TOPC:def 3;
then XX in the topology of ;
then XX in { (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact ) } by ;
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 ;
hence contradiction by A6, A12; :: thesis: verum
end;
[#] c= (Cl X9) \/ {([#] X)} by ;
hence [#] c= Cl X9 by ; :: thesis: verum
end;
given X9 being Subset of such that A13: X9 = [#] X and
A14: X9 is dense ; :: thesis: not X is compact
A15: Cl X9 = [#] 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 by ;
then reconsider X1 = {([#] X)} as Subset of ;
X1 is open by A16;
then A17: Cl (X1 `) = X1 ` by PRE_TOPC:22;
X1 ` = ([#] X) \ X1 by
.= [#] X by ;
hence contradiction by A13, A15, A17, A4; :: thesis: verum