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_{1} being Element of K19( the carrier of X) holds

( ( not b_{1} in the topology of X or ex b_{2} being Element of K19( the carrier of (One-Point_Compactification X)) st

( b_{2} in the topology of (One-Point_Compactification X) & b_{1} = b_{2} /\ ([#] X) ) ) & ( for b_{2} being Element of K19( the carrier of (One-Point_Compactification X)) holds

( not b_{2} in the topology of (One-Point_Compactification X) or not b_{1} = b_{2} /\ ([#] X) ) or b_{1} in the topology of X ) )

let P be Subset of X; :: thesis: ( ( not P in the topology of X or ex b_{1} being Element of K19( the carrier of (One-Point_Compactification X)) st

( b_{1} in the topology of (One-Point_Compactification X) & P = b_{1} /\ ([#] X) ) ) & ( for b_{1} being Element of K19( the carrier of (One-Point_Compactification X)) holds

( not b_{1} in the topology of (One-Point_Compactification X) or not P = b_{1} /\ ([#] 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;

A5: P = Q /\ ([#] X) ; :: thesis: P in the topology of 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

( ( not b

( b

( not b

let P be Subset of X; :: thesis: ( ( not P in the topology of X or ex b

( b

( not b

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_{1} being Element of K19( the carrier of (One-Point_Compactification X)) holds

( not b_{1} in the topology of (One-Point_Compactification X) or not P = b_{1} /\ ([#] X) ) or P in the topology of X )

given Q being Subset of (One-Point_Compactification X) such that A4:
Q in the topology of (One-Point_Compactification X)
and ( not b

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;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

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;

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;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