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