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:
reconsider aa = a as set by TARSKI:1;

A1: now :: thesis:

assume a in { (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact ) } ; :: thesis:
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:

proof

let A be object ; :: according to TARSKI:def 3 :: thesis:
assume A in aa ; :: thesis:
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:

end;

end;

assume a in the topology of X \/ { (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact ) } ; :: thesis:
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:

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₁ being strict TopStruct st
( the carrier of b₁ = succ ([#] X) & the topology of b₁ = the topology of X \/ { (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact ) } ) ; :: thesis: