set T = succ ([#] X);
set D = { (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact ) } ;
set O = the topology of X \/ { (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact ) } ;
the topology of X \/ { (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact ) } c= bool (succ ([#] X))

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in the topology of X \/ { (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact ) } or a in bool (succ ([#] X)) )
reconsider aa = a as set by TARSKI:1;

A1: now :: thesis: ( a in { (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact ) } implies aa c= succ ([#] X) )

assume a in { (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact ) } ; :: thesis: aa c= succ ([#] X)
then consider U being Subset of X such that
A2: a = U \/ {([#] X)} and
U is open and
U ` is compact ;
thus aa c= succ ([#] X) :: thesis: verum

proof

let A be object ; :: according to TARSKI:def 3 :: thesis: ( not A in aa or A in succ ([#] X) )
assume A in aa ; :: thesis: A in succ ([#] X)
then ( A in U or A in {([#] X)} ) by A2, XBOOLE_0:def 3;
hence A in succ ([#] X) by XBOOLE_0:def 3; :: thesis: verum

end;

end;

assume a in the topology of X \/ { (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact ) } ; :: thesis: a in bool (succ ([#] X))
then ( a in the topology of X or a in { (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact ) } ) by XBOOLE_0:def 3;
then a is Subset of (succ ([#] X)) by A1, XBOOLE_1:10;
hence a in bool (succ ([#] X)) ; :: thesis: verum

end;

then reconsider O = the topology of X \/ { (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact ) } as Subset-Family of (succ ([#] X)) ;
set Y = TopStruct(# (succ ([#] X)),O #);
not TopStruct(# (succ ([#] X)),O #) is empty ;
hence ex b<sub>1</sub> being strict TopStruct st
( the carrier of b<sub>1</sub> = succ ([#] X) & the topology of b<sub>1</sub> = the topology of X \/ { (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact ) } ) ; :: thesis: verum