let X be TopStruct ; :: thesis: X is SubSpace of One-Point_Compactification X
set D = { (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact ) } ;
thus A1: [#] X c= [#] (One-Point_Compactification X) by Th4; :: according to PRE_TOPC:def 4 :: thesis: for b1 being Element of K19( the carrier of X) holds
( ( not b1 in the topology of X or ex b2 being Element of K19( the carrier of (One-Point_Compactification X)) st
( b2 in the topology of (One-Point_Compactification X) & b1 = b2 /\ ([#] X) ) ) & ( for b2 being Element of K19( the carrier of (One-Point_Compactification X)) holds
( not b2 in the topology of (One-Point_Compactification X) or not b1 = b2 /\ ([#] X) ) or b1 in the topology of X ) )
let P be Subset of X; :: thesis: ( ( not P in the topology of X or ex b1 being Element of K19( the carrier of (One-Point_Compactification X)) st
( b1 in the topology of (One-Point_Compactification X) & P = b1 /\ ([#] X) ) ) & ( for b1 being Element of K19( the carrier of (One-Point_Compactification X)) holds
( not b1 in the topology of (One-Point_Compactification X) or not P = b1 /\ ([#] X) ) or P in the topology of X ) )
A2: 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;
hereby :: thesis: ( for b1 being Element of K19( the carrier of (One-Point_Compactification X)) holds
( not b1 in the topology of (One-Point_Compactification X) or not P = b1 /\ ([#] X) ) or P in the topology of X )
reconsider Q = P as Subset of (One-Point_Compactification X) by A1, XBOOLE_1:1;
assume A3: P in the topology of X ; :: thesis: ex Q being Subset of (One-Point_Compactification X) st
( Q in the topology of (One-Point_Compactification X) & P = Q /\ ([#] X) )
take Q = Q; :: thesis: ( Q in the topology of (One-Point_Compactification X) & P = Q /\ ([#] X) )
thus Q in the topology of (One-Point_Compactification X) by A2, A3, XBOOLE_0:def 3; :: thesis: P = Q /\ ([#] X)
thus P = Q /\ ([#] X) by XBOOLE_1:28; :: thesis: verum
end;
given Q being Subset of (One-Point_Compactification X) such that A4: Q in the topology of (One-Point_Compactification X) and
A5: P = Q /\ ([#] X) ; :: thesis: P in the topology of X
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 A2, A4, XBOOLE_0:def 3;
suppose Q in the topology of X ; :: thesis: P in the topology of X
hence P in the topology of X by A5, XBOOLE_1:28; :: thesis: verum
end;
suppose Q in { (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact ) } ; :: thesis: P in the topology of X
then consider U being Subset of X such that
A6: Q = U \/ {([#] X)} and
A7: 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 A5, A6, XBOOLE_1:23
.= U by XBOOLE_1:28 ;
hence P in the topology of X by A7; :: thesis: verum
end;
end;