let X be non empty TopSpace; :: thesis: ( not X is compact implies incl X,(One-Point_Compactification X) is compactification )
assume A1: not X is compact ; :: thesis: incl X,(One-Point_Compactification X) is compactification
set h = incl X,(One-Point_Compactification X);
A2: [#] X c= [#] (One-Point_Compactification X) by Th4;
then reconsider Xy = [#] X as Subset of (One-Point_Compactification X) ;
set D = { (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact ) } ;
A3: 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;
A4: [#] ((One-Point_Compactification X) | Xy) = Xy by PRE_TOPC:def 10;
the topology of ((One-Point_Compactification X) | Xy) = the topology of X

proof

thus the topology of ((One-Point_Compactification X) | Xy) c= the topology of X :: according to XBOOLE_0:def 10 :: thesis: the topology of X c= the topology of ((One-Point_Compactification X) | Xy)

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in the topology of ((One-Point_Compactification X) | Xy) or x in the topology of X )
assume A5: x in the topology of ((One-Point_Compactification X) | Xy) ; :: thesis: x in the topology of X
then reconsider P = x as Subset of ((One-Point_Compactification X) | Xy) ;
consider Q being Subset of (One-Point_Compactification X) such that
A6: Q in the topology of (One-Point_Compactification X) and
A7: P = Q /\ ([#] ((One-Point_Compactification X) | Xy)) by A5, PRE_TOPC:def 9;

per cases ( Q in the topology of X or Q in { (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact ) } ) by A3, A6, XBOOLE_0:def 3;

suppose Q in the topology of X ; :: thesis: x in the topology of X

hence x in the topology of X by A4, A7, XBOOLE_1:28; :: thesis: verum

end;

suppose Q in { (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact ) } ; :: thesis: x in the topology of X

then consider U being Subset of X such that
A8: Q = U \/ {([#] X)} and
A9: U is open and
U ` is compact ;
not [#] X in [#] X ;
then {([#] X)} misses [#] X by ZFMISC_1:56;
then {([#] X)} /\ ([#] X) = {} by XBOOLE_0:def 7;
then P = (U /\ ([#] X)) \/ {} by A4, A7, A8, XBOOLE_1:23
.= U by XBOOLE_1:28 ;
hence x in the topology of X by A9, PRE_TOPC:def 5; :: thesis: verum

end;

end;

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in the topology of X or x in the topology of ((One-Point_Compactification X) | Xy) )
assume A10: x in the topology of X ; :: thesis: x in the topology of ((One-Point_Compactification X) | Xy)
then reconsider P = x as Subset of ((One-Point_Compactification X) | Xy) by A4;
reconsider Q = P as Subset of (One-Point_Compactification X) by A4, XBOOLE_1:1;
A11: Q in the topology of (One-Point_Compactification X) by A3, A10, XBOOLE_0:def 3;
P = Q /\ ([#] ((One-Point_Compactification X) | Xy)) by XBOOLE_1:28;
hence x in the topology of ((One-Point_Compactification X) | Xy) by A11, PRE_TOPC:def 9; :: thesis: verum

end;

hence incl X,(One-Point_Compactification X) is embedding by A2, Th3; :: according to COMPACT1:def 8 :: thesis: ( One-Point_Compactification X is compact & (incl X,(One-Point_Compactification X)) .: ([#] X) is dense )
thus One-Point_Compactification X is compact ; :: thesis: (incl X,(One-Point_Compactification X)) .: ([#] X) is dense
ex X' being Subset of (One-Point_Compactification X) st
( X' = [#] X & X' is dense ) by A1, Th7;
hence (incl X,(One-Point_Compactification X)) .: ([#] X) is dense by A2, Th2; :: thesis: verum