let X be TopStruct ; :: thesis:
set D = { (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact ) } ;
thus A1: [#] X c= [#] 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 ) st
( b2 in the topology of & b1 = b2 /\ ([#] X) ) ) & ( for b2 being Element of K19( the carrier of ) holds
( not b2 in the topology of 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 ) st
( b1 in the topology of & P = b1 /\ ([#] X) ) ) & ( for b1 being Element of K19( the carrier of ) holds
( not b1 in the topology of or not P = b1 /\ ([#] X) ) or P in the topology of X ) )

A2: the topology of = 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 ) holds
( not b1 in the topology of or not P = b1 /\ ([#] X) ) or P in the topology of X )
reconsider Q = P as Subset of by ;
assume A3: P in the topology of X ; :: thesis: ex Q being Subset of st
( Q in the topology of & P = Q /\ ([#] X) )

take Q = Q; :: thesis: ( Q in the topology of & P = Q /\ ([#] X) )
thus Q in the topology of by ; :: thesis: P = Q /\ ([#] X)
thus P = Q /\ ([#] X) by XBOOLE_1:28; :: thesis: verum
end;
given Q being Subset of such that A4: Q in the topology of 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 ;
suppose Q in the topology of X ; :: thesis: P in the topology of X
hence P in the topology of X by ; :: 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
.= U by XBOOLE_1:28 ;
hence P in the topology of X by A7; :: thesis: verum
end;
end;