let X be non empty TopSpace; :: thesis: ( not X is compact implies incl (X,(One-Point_Compactification X)) is compactification )
set h = incl (X,(One-Point_Compactification X));
set D = { (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact ) } ;
assume not X is compact ; :: thesis: incl (X,(One-Point_Compactification X)) is compactification
then A1: ex X9 being Subset of (One-Point_Compactification X) st
( X9 = [#] X & X9 is dense ) by Th7;
A2: [#] X c= [#] (One-Point_Compactification X) by Th4;
then reconsider Xy = [#] X as Subset of (One-Point_Compactification X) ;
A3: [#] ((One-Point_Compactification X) | Xy) = Xy by PRE_TOPC:def 5;
A4: 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;
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 object ; :: 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 4;
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 A4, 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 A3, 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:50;
then {([#] X)} /\ ([#] X) = {} ;
then P = (U /\ ([#] X)) \/ {} by A3, A7, A8, XBOOLE_1:23
.= U by XBOOLE_1:28 ;
hence x in the topology of X by A9; :: thesis: verum
end;
end;
end;
let x be object ; :: 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 A3;
reconsider Q = P as Subset of (One-Point_Compactification X) by A3, XBOOLE_1:1;
A11: P = Q /\ ([#] ((One-Point_Compactification X) | Xy)) by XBOOLE_1:28;
Q in the topology of (One-Point_Compactification X) by A4, A10, XBOOLE_0:def 3;
hence x in the topology of ((One-Point_Compactification X) | Xy) by A11, PRE_TOPC:def 4; :: 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
thus (incl (X,(One-Point_Compactification X))) .: ([#] X) is dense by A1, Th2; :: thesis: verum