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 b<sub>1</sub> being Element of K19( the carrier of X) holds
( ( not b<sub>1</sub> in the topology of X or ex b<sub>2</sub> being Element of K19( the carrier of (One-Point_Compactification X)) st
( b<sub>2</sub> in the topology of (One-Point_Compactification X) & b<sub>1</sub> = b<sub>2</sub> /\ ([#] X) ) ) & ( for b<sub>2</sub> being Element of K19( the carrier of (One-Point_Compactification X)) holds
( not b<sub>2</sub> in the topology of (One-Point_Compactification X) or not b<sub>1</sub> = b<sub>2</sub> /\ ([#] X) ) or b<sub>1</sub> in the topology of X ) )
let P be Subset of X; :: thesis: ( ( not P in the topology of X or ex b<sub>1</sub> being Element of K19( the carrier of (One-Point_Compactification X)) st
( b<sub>1</sub> in the topology of (One-Point_Compactification X) & P = b<sub>1</sub> /\ ([#] X) ) ) & ( for b<sub>1</sub> being Element of K19( the carrier of (One-Point_Compactification X)) holds
( not b<sub>1</sub> in the topology of (One-Point_Compactification X) or not P = b<sub>1</sub> /\ ([#] 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 b₁ being Element of K19( the carrier of (One-Point_Compactification X)) holds
( not b₁ in the topology of (One-Point_Compactification X) or not P = b₁ /\ ([#] 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;