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

set Y = TopStruct(# (succ ([#] X)),O #);

not TopStruct(# (succ ([#] X)),O #) is empty ;

hence ex b_{1} being strict TopStruct st

( the carrier of b_{1} = succ ([#] X) & the topology of b_{1} = the topology of X \/ { (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact ) } )
; :: thesis: verum

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

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

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

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

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

set Y = TopStruct(# (succ ([#] X)),O #);

not TopStruct(# (succ ([#] X)),O #) is empty ;

hence ex b

( the carrier of b