:: COMPACT1 semantic presentation

K104() is Element of K19(K100())
K100() is set
K19(K100()) is non empty V21() V23() V24() set
omega is set
K19(omega) is non empty V21() V23() V24() set
K19(K104()) is non empty V21() V23() V24() set
K95(K104()) is non empty V21() V23() V24() set

1 is non empty set

the carrier of X is set
K19( the carrier of X) is non empty V21() V23() V24() set
K19(K19( the carrier of X)) is non empty V21() V23() V24() set

the carrier of X is set
K19( the carrier of X) is non empty V21() V23() V24() set

the carrier of X is set
K19( the carrier of X) is non empty V21() V23() V24() set
h is Element of K19( the carrier of X)
Cl h is closed Element of K19( the carrier of X)

the carrier of X is set
K19( the carrier of X) is non empty V21() V23() V24() set

the carrier of X is set
K19( the carrier of X) is non empty V21() V23() V24() set
h is (X) Element of K19( the carrier of X)
Cl h is closed Element of K19( the carrier of X)

the carrier of X is set
K19( the carrier of X) is non empty V21() V23() V24() set
X is non empty TopSpace-like TopStruct
the carrier of X is non empty set
h is Element of the carrier of X
{ b1 where b1 is a_neighborhood of h : ( b1 is compact & ex b2 being a_neighborhood of h st b1 c= b2 ) } is set
[#] X is non empty non proper open closed dense non boundary Element of K19( the carrier of X)
K19( the carrier of X) is non empty V21() V23() V24() set
bool ([#] X) is non empty V21() V23() V24() Element of K19(K19(([#] X)))
K19(([#] X)) is non empty V21() V23() V24() set
K19(K19(([#] X))) is non empty V21() V23() V24() set
Xy is set
x is a_neighborhood of h
P is a_neighborhood of h
K19(K19( the carrier of X)) is non empty V21() V23() V24() set
Xy is Element of K19(K19( the carrier of X))
x is a_neighborhood of h
Int x is open Element of K19( the carrier of X)
x ` is Element of K19( the carrier of X)
the carrier of X \ x is set
Cl (x `) is closed Element of K19( the carrier of X)
(Cl (x `)) ` is open Element of K19( the carrier of X)
the carrier of X \ (Cl (x `)) is set
P is Element of K19( the carrier of X)
Int P is open Element of K19( the carrier of X)
P ` is Element of K19( the carrier of X)
the carrier of X \ P is set
Cl (P `) is closed Element of K19( the carrier of X)
(Cl (P `)) ` is open Element of K19( the carrier of X)
the carrier of X \ (Cl (P `)) is set
Q is a_neighborhood of h
x is Element of K19( the carrier of X)
P is a_neighborhood of h
Q is a_neighborhood of h
h is Element of the carrier of X
D is Element of K19( the carrier of X)
Xy is non empty basis of h
Int D is open Element of K19( the carrier of X)
D ` is Element of K19( the carrier of X)
the carrier of X \ D is set
Cl (D `) is closed Element of K19( the carrier of X)
(Cl (D `)) ` is open Element of K19( the carrier of X)
the carrier of X \ (Cl (D `)) is set
x is Element of K19( the carrier of X)
Int x is open Element of K19( the carrier of X)
x ` is Element of K19( the carrier of X)
the carrier of X \ x is set
Cl (x `) is closed Element of K19( the carrier of X)
(Cl (x `)) ` is open Element of K19( the carrier of X)
the carrier of X \ (Cl (x `)) is set
X is non empty TopSpace-like TopStruct
the carrier of X is non empty set
h is Element of the carrier of X
D is non empty basis of h
the a_neighborhood of h is a_neighborhood of h
x is a_neighborhood of h
X is non empty TopSpace-like regular TopStruct
the carrier of X is non empty set
h is Element of the carrier of X
K19( the carrier of X) is non empty V21() V23() V24() set
{ b1 where b1 is a_neighborhood of h : ( b1 is compact & ex b2, b3 being a_neighborhood of h st b1 c= b2 /\ b3 ) } is set
[#] X is non empty non proper open closed dense non boundary Element of K19( the carrier of X)
bool ([#] X) is non empty V21() V23() V24() Element of K19(K19(([#] X)))
K19(([#] X)) is non empty V21() V23() V24() set
K19(K19(([#] X))) is non empty V21() V23() V24() set
Xy is set
x is a_neighborhood of h
P is a_neighborhood of h
Q is a_neighborhood of h
P /\ Q is Element of K19( the carrier of X)
K19(K19( the carrier of X)) is non empty V21() V23() V24() set
Xy is Element of K19(K19( the carrier of X))
x is a_neighborhood of h
Int x is open Element of K19( the carrier of X)
x ` is Element of K19( the carrier of X)
the carrier of X \ x is set
Cl (x `) is closed Element of K19( the carrier of X)
(Cl (x `)) ` is open Element of K19( the carrier of X)
the carrier of X \ (Cl (x `)) is set
P is a_neighborhood of h
Int P is open Element of K19( the carrier of X)
P ` is Element of K19( the carrier of X)
the carrier of X \ P is set
Cl (P `) is closed Element of K19( the carrier of X)
(Cl (P `)) ` is open Element of K19( the carrier of X)
the carrier of X \ (Cl (P `)) is set
(Int x) /\ (Int P) is open Element of K19( the carrier of X)
x /\ P is Element of K19( the carrier of X)
Int (x /\ P) is open Element of K19( the carrier of X)
(x /\ P) ` is Element of K19( the carrier of X)
the carrier of X \ (x /\ P) is set
Cl ((x /\ P) `) is closed Element of K19( the carrier of X)
(Cl ((x /\ P) `)) ` is open Element of K19( the carrier of X)
the carrier of X \ (Cl ((x /\ P) `)) is set
Q is Element of K19( the carrier of X)
Int Q is open Element of K19( the carrier of X)
Q ` is Element of K19( the carrier of X)
the carrier of X \ Q is set
Cl (Q `) is closed Element of K19( the carrier of X)
(Cl (Q `)) ` is open Element of K19( the carrier of X)
the carrier of X \ (Cl (Q `)) is set
U is a_neighborhood of h
x is Element of K19( the carrier of X)
P is a_neighborhood of h
Q is a_neighborhood of h
U is a_neighborhood of h
Q /\ U is Element of K19( the carrier of X)
X is non empty TopSpace-like TopStruct
the carrier of X is non empty set
h is Element of the carrier of X
D is a_neighborhood of h
Int D is open Element of K19( the carrier of X)
K19( the carrier of X) is non empty V21() V23() V24() set
D ` is Element of K19( the carrier of X)
the carrier of X \ D is set
Cl (D `) is closed Element of K19( the carrier of X)
(Cl (D `)) ` is open Element of K19( the carrier of X)
the carrier of X \ (Cl (D `)) is set
Cl D is closed Element of K19( the carrier of X)
Int (Cl D) is open Element of K19( the carrier of X)
(Cl D) ` is open Element of K19( the carrier of X)
the carrier of X \ (Cl D) is set
Cl ((Cl D) `) is closed Element of K19( the carrier of X)
(Cl ((Cl D) `)) ` is open Element of K19( the carrier of X)
the carrier of X \ (Cl ((Cl D) `)) is set
X is non empty TopSpace-like TopStruct
the carrier of X is non empty set
h is Element of the carrier of X
D is a_neighborhood of h
Cl D is closed Element of K19( the carrier of X)
K19( the carrier of X) is non empty V21() V23() V24() set
X is non empty TopSpace-like TopStruct
the carrier of X is non empty set
h is Element of the carrier of X
D is a_neighborhood of h
Int D is open Element of K19( the carrier of X)
K19( the carrier of X) is non empty V21() V23() V24() set
D ` is Element of K19( the carrier of X)
the carrier of X \ D is set
Cl (D `) is closed Element of K19( the carrier of X)
(Cl (D `)) ` is open Element of K19( the carrier of X)
the carrier of X \ (Cl (D `)) is set
Cl D is closed Element of K19( the carrier of X)
Int (Cl D) is open Element of K19( the carrier of X)
(Cl D) ` is open Element of K19( the carrier of X)
the carrier of X \ (Cl D) is set
Cl ((Cl D) `) is closed Element of K19( the carrier of X)
(Cl ((Cl D) `)) ` is open Element of K19( the carrier of X)
the carrier of X \ (Cl ((Cl D) `)) is set
X is non empty TopSpace-like T_0 T_1 T_2 TopStruct
the carrier of X is non empty set
h is Element of the carrier of X
D is a_neighborhood of h
Cl D is closed Element of K19( the carrier of X)
K19( the carrier of X) is non empty V21() V23() V24() set
X is non empty TopSpace-like TopStruct
[#] X is non empty non proper open closed dense non boundary Element of K19( the carrier of X)
the carrier of X is non empty set
K19( the carrier of X) is non empty V21() V23() V24() set
D is Element of the carrier of X
Int ([#] X) is open Element of K19( the carrier of X)
([#] X) ` is open closed Element of K19( the carrier of X)
the carrier of X \ ([#] X) is set
Cl (([#] X) `) is closed Element of K19( the carrier of X)
(Cl (([#] X) `)) ` is open Element of K19( the carrier of X)
the carrier of X \ (Cl (([#] X) `)) is set
X is non empty TopSpace-like TopStruct
the carrier of X is non empty set
h is Element of the carrier of X
{h} is non empty finite compact Element of K19( the carrier of X)
K19( the carrier of X) is non empty V21() V23() V24() set
Int {h} is open Element of K19( the carrier of X)
{h} ` is Element of K19( the carrier of X)
the carrier of X \ {h} is set
Cl ({h} `) is closed Element of K19( the carrier of X)
(Cl ({h} `)) ` is open Element of K19( the carrier of X)
the carrier of X \ (Cl ({h} `)) is set
Xy is a_neighborhood of h

X is non empty TopSpace-like () TopStruct
the carrier of X is non empty set
K19( the carrier of X) is non empty V21() V23() V24() set
h is non empty closed Element of K19( the carrier of X)
X | h is non empty strict TopSpace-like SubSpace of X
the carrier of (X | h) is non empty set
D is Element of the carrier of (X | h)
Xy is Element of the carrier of X
x is a_neighborhood of Xy
[#] (X | h) is non empty non proper open closed dense non boundary Element of K19( the carrier of (X | h))
K19( the carrier of (X | h)) is non empty V21() V23() V24() set
x /\ h is Element of K19( the carrier of X)
P is Element of K19( the carrier of (X | h))
Q is a_neighborhood of D
Int x is open Element of K19( the carrier of X)
x ` is Element of K19( the carrier of X)
the carrier of X \ x is set
Cl (x `) is closed Element of K19( the carrier of X)
(Cl (x `)) ` is open Element of K19( the carrier of X)
the carrier of X \ (Cl (x `)) is set
X | x is strict TopSpace-like SubSpace of X
[#] (X | x) is non proper open closed dense Element of K19( the carrier of (X | x))
the carrier of (X | x) is set
K19( the carrier of (X | x)) is non empty V21() V23() V24() set
U is Element of K19( the carrier of (X | x))
(X | x) | U is strict TopSpace-like SubSpace of X | x
X | (x /\ h) is strict TopSpace-like SubSpace of X
(X | h) | Q is strict TopSpace-like SubSpace of X | h

the carrier of X is non empty set
K19( the carrier of X) is non empty V21() V23() V24() set
h is non empty open Element of K19( the carrier of X)
X | h is non empty strict TopSpace-like SubSpace of X
the carrier of (X | h) is non empty set
D is Element of the carrier of (X | h)
Xy is Element of the carrier of X
x is non empty basis of Xy
[#] (X | h) is non empty non proper open closed dense non boundary Element of K19( the carrier of (X | h))
K19( the carrier of (X | h)) is non empty V21() V23() V24() set
Int h is open Element of K19( the carrier of X)
h ` is closed Element of K19( the carrier of X)
the carrier of X \ h is set
Cl (h `) is closed Element of K19( the carrier of X)
(Cl (h `)) ` is open Element of K19( the carrier of X)
the carrier of X \ (Cl (h `)) is set
P is a_neighborhood of Xy
Q is Element of K19( the carrier of (X | h))
Int P is open Element of K19( the carrier of X)
P ` is Element of K19( the carrier of X)
the carrier of X \ P is set
Cl (P `) is closed Element of K19( the carrier of X)
(Cl (P `)) ` is open Element of K19( the carrier of X)
the carrier of X \ (Cl (P `)) is set
P /\ h is Element of K19( the carrier of X)
X is non empty TopSpace-like T_0 T_1 T_2 TopStruct
the carrier of X is non empty set
K19( the carrier of X) is non empty V21() V23() V24() set
h is non empty Element of K19( the carrier of X)
X | h is non empty strict TopSpace-like T_0 T_1 T_2 SubSpace of X
[#] (X | h) is non empty non proper open closed dense non boundary Element of K19( the carrier of (X | h))
the carrier of (X | h) is non empty set
K19( the carrier of (X | h)) is non empty V21() V23() V24() set
Int h is open Element of K19( the carrier of X)
h ` is Element of K19( the carrier of X)
the carrier of X \ h is set
Cl (h `) is closed Element of K19( the carrier of X)
(Cl (h `)) ` is open Element of K19( the carrier of X)
the carrier of X \ (Cl (h `)) is set
D is set
Xy is Element of the carrier of X
{ b1 where b1 is Element of K19( the carrier of X) : ( b1 is open & b1 c= h ) } is set
x is Element of the carrier of (X | h)
Q is a_neighborhood of x
Int Q is open Element of K19( the carrier of (X | h))
Q ` is Element of K19( the carrier of (X | h))
the carrier of (X | h) \ Q is set
Cl (Q `) is closed Element of K19( the carrier of (X | h))
(Cl (Q `)) ` is open Element of K19( the carrier of (X | h))
the carrier of (X | h) \ (Cl (Q `)) is set
the topology of (X | h) is non empty open Element of K19(K19( the carrier of (X | h)))
K19(K19( the carrier of (X | h))) is non empty V21() V23() V24() set
the topology of X is non empty open Element of K19(K19( the carrier of X))
K19(K19( the carrier of X)) is non empty V21() V23() V24() set
Vx is Element of K19( the carrier of X)
Vx /\ h is Element of K19( the carrier of X)
U is Element of K19( the carrier of X)
K is Element of K19( the carrier of (X | h))
Cl (Vx /\ h) is closed Element of K19( the carrier of X)
Cl Vx is closed Element of K19( the carrier of X)
union { b1 where b1 is Element of K19( the carrier of X) : ( b1 is open & b1 c= h ) } is set

the carrier of X is set
K19( the carrier of X) is non empty V21() V23() V24() set
[#] X is non proper open closed dense Element of K19( the carrier of X)

[#] h is non proper open closed dense Element of K19( the carrier of h)
the carrier of h is set
K19( the carrier of h) is non empty V21() V23() V24() set
incl (X,h) is Relation-like the carrier of X -defined the carrier of h -valued Function-like V18( the carrier of X, the carrier of h) Element of K19(K20( the carrier of X, the carrier of h))
K20( the carrier of X, the carrier of h) is Relation-like set
K19(K20( the carrier of X, the carrier of h)) is non empty V21() V23() V24() set
D is Element of K19( the carrier of X)
(incl (X,h)) .: D is Element of K19( the carrier of h)

(id ([#] X)) .: D is set

the carrier of X is set

the carrier of h is set
K20( the carrier of X, the carrier of h) is Relation-like set
K19(K20( the carrier of X, the carrier of h)) is non empty V21() V23() V24() set

[#] X is non proper open closed dense Element of K19( the carrier of X)
the carrier of X is set
K19( the carrier of X) is non empty V21() V23() V24() set

[#] h is non proper open closed dense Element of K19( the carrier of h)
the carrier of h is set
K19( the carrier of h) is non empty V21() V23() V24() set
the topology of X is non empty open Element of K19(K19( the carrier of X))
K19(K19( the carrier of X)) is non empty V21() V23() V24() set
incl (X,h) is Relation-like the carrier of X -defined the carrier of h -valued Function-like V18( the carrier of X, the carrier of h) Element of K19(K20( the carrier of X, the carrier of h))
K20( the carrier of X, the carrier of h) is Relation-like set
K19(K20( the carrier of X, the carrier of h)) is non empty V21() V23() V24() set
id X is Relation-like the carrier of X -defined the carrier of X -valued Function-like V18( the carrier of X, the carrier of X) continuous V151(X,X) Element of K19(K20( the carrier of X, the carrier of X))
K20( the carrier of X, the carrier of X) is Relation-like set
K19(K20( the carrier of X, the carrier of X)) is non empty V21() V23() V24() set
K38( the carrier of X) is Relation-like the carrier of X -defined the carrier of X -valued Function-like one-to-one V14( the carrier of X) Element of K19(K20( the carrier of X, the carrier of X))
rng (incl (X,h)) is Element of K19( the carrier of h)
h | (rng (incl (X,h))) is strict TopSpace-like SubSpace of h
[#] (h | (rng (incl (X,h)))) is non proper open closed dense Element of K19( the carrier of (h | (rng (incl (X,h)))))
the carrier of (h | (rng (incl (X,h)))) is set
K19( the carrier of (h | (rng (incl (X,h))))) is non empty V21() V23() V24() set
K20( the carrier of X, the carrier of (h | (rng (incl (X,h))))) is Relation-like set
K19(K20( the carrier of X, the carrier of (h | (rng (incl (X,h)))))) is non empty V21() V23() V24() set
P is Element of K19( the carrier of h)
h | P is strict TopSpace-like SubSpace of h
the topology of (h | P) is non empty open Element of K19(K19( the carrier of (h | P)))
the carrier of (h | P) is set
K19( the carrier of (h | P)) is non empty V21() V23() V24() set
K19(K19( the carrier of (h | P))) is non empty V21() V23() V24() set
Xy is Relation-like the carrier of X -defined the carrier of (h | (rng (incl (X,h)))) -valued Function-like V18( the carrier of X, the carrier of (h | (rng (incl (X,h))))) Element of K19(K20( the carrier of X, the carrier of (h | (rng (incl (X,h))))))
Xy " is Relation-like the carrier of (h | (rng (incl (X,h)))) -defined the carrier of X -valued Function-like V18( the carrier of (h | (rng (incl (X,h)))), the carrier of X) Element of K19(K20( the carrier of (h | (rng (incl (X,h)))), the carrier of X))
K20( the carrier of (h | (rng (incl (X,h)))), the carrier of X) is Relation-like set
K19(K20( the carrier of (h | (rng (incl (X,h)))), the carrier of X)) is non empty V21() V23() V24() set
Q is Element of K19( the carrier of X)
(Xy ") " Q is Element of K19( the carrier of (h | (rng (incl (X,h)))))
U is Element of K19( the carrier of (h | (rng (incl (X,h)))))
Xy .: U is Element of K19( the carrier of (h | (rng (incl (X,h)))))
the topology of (h | (rng (incl (X,h)))) is non empty open Element of K19(K19( the carrier of (h | (rng (incl (X,h))))))
K19(K19( the carrier of (h | (rng (incl (X,h)))))) is non empty V21() V23() V24() set
Q is Element of K19( the carrier of (h | (rng (incl (X,h)))))
Xy " Q is Element of K19( the carrier of X)
the topology of (h | (rng (incl (X,h)))) is non empty open Element of K19(K19( the carrier of (h | (rng (incl (X,h))))))
K19(K19( the carrier of (h | (rng (incl (X,h)))))) is non empty V21() V23() V24() set
U is Element of K19( the carrier of X)
(id X) " U is Element of K19( the carrier of X)
dom Xy is Element of K19( the carrier of X)
rng Xy is Element of K19( the carrier of (h | (rng (incl (X,h)))))

the carrier of X is set

the carrier of h is set
K20( the carrier of X, the carrier of h) is Relation-like set
K19(K20( the carrier of X, the carrier of h)) is non empty V21() V23() V24() set

the carrier of X is set

the carrier of h is set
K20( the carrier of X, the carrier of h) is Relation-like set
K19(K20( the carrier of X, the carrier of h)) is non empty V21() V23() V24() set
D is Relation-like the carrier of X -defined the carrier of h -valued Function-like V18( the carrier of X, the carrier of h) Element of K19(K20( the carrier of X, the carrier of h))
X is TopStruct
[#] X is non proper dense Element of K19( the carrier of X)
the carrier of X is set
K19( the carrier of X) is non empty V21() V23() V24() set
succ ([#] X) is set
{([#] X)} is non empty finite set
([#] X) \/ {([#] X)} is non empty set
the topology of X is open Element of K19(K19( the carrier of X))
K19(K19( the carrier of X)) is non empty V21() V23() V24() set
{([#] X)} is non empty finite Element of K19(K19( the carrier of X))
{ (b1 \/ {([#] X)}) where b1 is Element of K19( the carrier of X) : ( b1 is open & b1 ` is compact ) } is set
the topology of X \/ { (b1 \/ {([#] X)}) where b1 is Element of K19( the carrier of X) : ( b1 is open & b1 ` is compact ) } is set
bool (succ ([#] X)) is non empty V21() V23() V24() Element of K19(K19((succ ([#] X))))
K19((succ ([#] X))) is non empty V21() V23() V24() set
K19(K19((succ ([#] X)))) is non empty V21() V23() V24() set
x is set
P is Element of K19( the carrier of X)
P \/ {([#] X)} is non empty set
P ` is Element of K19( the carrier of X)
the carrier of X \ P is set
Q is set
x is Element of K19(K19((succ ([#] X))))
TopStruct(# (succ ([#] X)),x #) is strict TopStruct

the carrier of h is set
the topology of h is open Element of K19(K19( the carrier of h))
K19( the carrier of h) is non empty V21() V23() V24() set
K19(K19( the carrier of h)) is non empty V21() V23() V24() set

the carrier of D is set
the topology of D is open Element of K19(K19( the carrier of D))
K19( the carrier of D) is non empty V21() V23() V24() set
K19(K19( the carrier of D)) is non empty V21() V23() V24() set
X is TopStruct
(X) is strict TopStruct
the carrier of (X) is set
[#] X is non proper dense Element of K19( the carrier of X)
the carrier of X is set
K19( the carrier of X) is non empty V21() V23() V24() set
succ ([#] X) is set
{([#] X)} is non empty finite set
([#] X) \/ {([#] X)} is non empty set
X is TopStruct
[#] X is non proper dense Element of K19( the carrier of X)
the carrier of X is set
K19( the carrier of X) is non empty V21() V23() V24() set
(X) is non empty strict TopStruct
[#] (X) is non empty non proper dense Element of K19( the carrier of (X))
the carrier of (X) is non empty set
K19( the carrier of (X)) is non empty V21() V23() V24() set
succ ([#] X) is set
{([#] X)} is non empty finite set
([#] X) \/ {([#] X)} is non empty set

(X) is non empty strict TopStruct
[#] X is non proper open closed dense Element of K19( the carrier of X)
the carrier of X is set
K19( the carrier of X) is non empty V21() V23() V24() set
succ ([#] X) is set
{([#] X)} is non empty finite set
([#] X) \/ {([#] X)} is non empty set
{([#] X)} is non empty finite Element of K19(K19( the carrier of X))
K19(K19( the carrier of X)) is non empty V21() V23() V24() set
{ (b1 \/ {([#] X)}) where b1 is Element of K19( the carrier of X) : ( b1 is open & b1 ` is compact ) } is set
the topology of (X) is open Element of K19(K19( the carrier of (X)))
the carrier of (X) is non empty set
K19( the carrier of (X)) is non empty V21() V23() V24() set
K19(K19( the carrier of (X))) is non empty V21() V23() V24() set
the topology of X is non empty open Element of K19(K19( the carrier of X))
the topology of X \/ { (b1 \/ {([#] X)}) where b1 is Element of K19( the carrier of X) : ( b1 is open & b1 ` is compact ) } is non empty set
[#] (X) is non empty non proper dense Element of K19( the carrier of (X))
([#] X) ` is open closed Element of K19( the carrier of X)
the carrier of X \ ([#] X) is set

({} X) ` is open closed dense Element of K19( the carrier of X)
the carrier of X \ ({} X) is set
(({} X) `) ` is open closed Element of K19( the carrier of X)
the carrier of X \ (({} X) `) is set
x is Element of K19(K19( the carrier of (X)))
{ b1 where b1 is Element of K19( the carrier of X) : ( b1 is open & ( b1 in x or b1 \/ {([#] X)} in x ) ) } is set
Q is set
U is Element of K19( the carrier of X)
U \/ {([#] X)} is non empty set
Q is Element of K19(K19( the carrier of X))
union Q is Element of K19( the carrier of X)
union x is Element of K19( the carrier of (X))
() \ {([#] X)} is Element of K19( the carrier of (X))
U is set
Vx is set
K is Element of K19( the carrier of X)
K \/ {([#] X)} is non empty set
U is set
Vx is set
K is Element of K19( the carrier of X)
K is Element of K19( the carrier of X)
K \/ {([#] X)} is non empty set
K ` is Element of K19( the carrier of X)
the carrier of X \ K is set
U is set
Vx is Element of K19( the carrier of X)
Vx \/ {([#] X)} is non empty set
Vx ` is Element of K19( the carrier of X)
the carrier of X \ Vx is set
U \ {([#] X)} is Element of K19(U)
K19(U) is non empty V21() V23() V24() set
Vx \ {([#] X)} is Element of K19( the carrier of X)
() ` is Element of K19( the carrier of X)
the carrier of X \ () is set
() \/ {([#] X)} is non empty set
() \/ {([#] X)} is non empty set
U is set
Vx is Element of K19( the carrier of X)
Vx \/ {([#] X)} is non empty set
Vx ` is Element of K19( the carrier of X)
the carrier of X \ Vx is set
K19(([#] X)) is non empty V21() V23() V24() set
K19(K19(([#] X))) is non empty V21() V23() V24() set
x is Element of K19( the carrier of (X))
P is Element of K19( the carrier of (X))
x /\ P is Element of K19( the carrier of (X))
x /\ P is Element of K19( the carrier of (X))
Q is Element of K19( the carrier of X)
Q /\ {([#] X)} is finite Element of K19(K19( the carrier of X))
Vx is Element of K19( the carrier of X)
Vx \/ {([#] X)} is non empty set
Vx ` is Element of K19( the carrier of X)
the carrier of X \ Vx is set
Q /\ Vx is Element of K19( the carrier of X)
x /\ P is Element of K19( the carrier of (X))
K is open Element of K19( the carrier of X)
U is open Element of K19( the carrier of X)
K \/ U is open Element of K19( the carrier of X)
Q is Element of K19( the carrier of X)
Q /\ {([#] X)} is finite Element of K19(K19( the carrier of X))
Vx is Element of K19( the carrier of X)
Vx \/ {([#] X)} is non empty set
Vx ` is Element of K19( the carrier of X)
the carrier of X \ Vx is set
Q /\ Vx is Element of K19( the carrier of X)
x /\ P is Element of K19( the carrier of (X))
K is open Element of K19( the carrier of X)
U is open Element of K19( the carrier of X)
K \/ U is open Element of K19( the carrier of X)
Q is Element of K19( the carrier of X)
Q \/ {([#] X)} is non empty set
Q ` is Element of K19( the carrier of X)
the carrier of X \ Q is set
U is Element of K19( the carrier of X)
U \/ {([#] X)} is non empty set
U ` is Element of K19( the carrier of X)
the carrier of X \ U is set
(Q `) \/ (U `) is Element of K19( the carrier of X)
Q /\ U is Element of K19( the carrier of X)
(Q /\ U) ` is Element of K19( the carrier of X)
the carrier of X \ (Q /\ U) is set
x /\ P is Element of K19( the carrier of (X))
(Q /\ U) \/ {([#] X)} is non empty set
X is TopStruct
(X) is non empty strict TopStruct
the carrier of X is set
K19( the carrier of X) is non empty V21() V23() V24() set
[#] X is non proper dense Element of K19( the carrier of X)
{([#] X)} is non empty finite Element of K19(K19( the carrier of X))
K19(K19( the carrier of X)) is non empty V21() V23() V24() set
{ (b1 \/ {([#] X)}) where b1 is Element of K19( the carrier of X) : ( b1 is open & b1 ` is compact ) } is set
[#] (X) is non empty non proper dense Element of K19( the carrier of (X))
the carrier of (X) is non empty set
K19( the carrier of (X)) is non empty V21() V23() V24() set
the topology of X is open Element of K19(K19( the carrier of X))
the topology of (X) is open Element of K19(K19( the carrier of (X)))
K19(K19( the carrier of (X))) is non empty V21() V23() V24() set
D is Element of K19( the carrier of X)
the topology of X \/ { (b1 \/ {([#] X)}) where b1 is Element of K19( the carrier of X) : ( b1 is open & b1 ` is compact ) } is set
Xy is Element of K19( the carrier of (X))
x is Element of K19( the carrier of (X))
x /\ ([#] X) is Element of K19( the carrier of X)
Xy is Element of K19( the carrier of (X))
Xy /\ ([#] X) is Element of K19( the carrier of X)
x is Element of K19( the carrier of X)
x \/ {([#] X)} is non empty set
x ` is Element of K19( the carrier of X)
the carrier of X \ x is set
{([#] X)} /\ ([#] X) is finite Element of K19( the carrier of X)
x /\ ([#] X) is Element of K19( the carrier of X)
(x /\ ([#] X)) \/ {} is set

(X) is non empty strict TopSpace-like TopStruct
the carrier of X is set
K19( the carrier of X) is non empty V21() V23() V24() set
[#] X is non proper open closed dense Element of K19( the carrier of X)
{([#] X)} is non empty finite Element of K19(K19( the carrier of X))
K19(K19( the carrier of X)) is non empty V21() V23() V24() set
{ (b1 \/ {([#] X)}) where b1 is Element of K19( the carrier of X) : ( b1 is open & b1 ` is compact ) } is set
the carrier of (X) is non empty set
K19( the carrier of (X)) is non empty V21() V23() V24() set
K19(K19( the carrier of (X))) is non empty V21() V23() V24() set
D is Element of K19(K19( the carrier of (X)))
[#] (X) is non empty non proper open closed dense non boundary Element of K19( the carrier of (X))
union D is Element of K19( the carrier of (X))
{ b1 where b1 is Element of K19( the carrier of X) : ( b1 is open & ( ( b1 in D & not b1 \/ {([#] X)} in D ) or b1 \/ {([#] X)} in D ) ) } is set
the topology of X is non empty open Element of K19(K19( the carrier of X))
x is set
P is Element of K19( the carrier of X)
P \/ {([#] X)} is non empty set
x is Element of K19(K19( the carrier of X))
P is Element of K19( the carrier of X)
Q is Element of K19( the carrier of X)
Q \/ {([#] X)} is non empty set
succ ([#] X) is set
{([#] X)} is non empty finite set
([#] X) \/ {([#] X)} is non empty set
P is set
Q is Element of K19( the carrier of (X))
the topology of (X) is non empty open Element of K19(K19( the carrier of (X)))
the topology of X \/ { (b1 \/ {([#] X)}) where b1 is Element of K19( the carrier of X) : ( b1 is open & b1 ` is compact ) } is non empty set
U is Element of K19( the carrier of X)
U \/ {([#] X)} is non empty set
U ` is Element of K19( the carrier of X)
the carrier of X \ U is set
Vx is set
union x is set
K is set
K is Element of K19( the carrier of (X))
c12 is Element of K19( the carrier of X)
c12 \/ {([#] X)} is non empty set
union x is Element of K19( the carrier of X)
c12 is Element of K19( the carrier of X)
c12 \/ {([#] X)} is non empty set
c12 ` is Element of K19( the carrier of X)
the carrier of X \ c12 is set
union x is Element of K19( the carrier of X)
union x is Element of K19( the carrier of X)
Vx is Element of K19(K19( the carrier of X))
{ b1 where b1 is Element of K19( the carrier of (X)) : ( b1 in D & ex b2 being Element of K19( the carrier of X) st
( b2 in Vx & ( ( b2 in D & not b2 \/ {([#] X)} in D & b1 = b2 ) or ( b2 \/ {([#] X)} in D & b1 = b2 \/ {([#] X)} ) ) ) )
}
is set

K is set
c12 is Element of K19( the carrier of (X))
K is set
K \/ {([#] X)} is non empty set
c12 is Element of K19( the carrier of X)
c12 \/ {([#] X)} is non empty set
G is Element of K19( the carrier of (X))
G is Element of K19( the carrier of (X))

dom K is set
rng K is set
c12 is set
G is Element of K19( the carrier of (X))
P is Element of K19( the carrier of X)
P \/ {([#] X)} is non empty set
P is Element of K19( the carrier of X)
P \/ {([#] X)} is non empty set
K . P is set
c12 is finite Element of K19(K19( the carrier of (X)))
{Q} is non empty finite Element of K19(K19( the carrier of (X)))
c12 \/ {Q} is non empty finite Element of K19(K19( the carrier of (X)))
G is non empty finite Element of K19(K19( the carrier of (X)))
P is set
z is Element of K19( the carrier of (X))
S is Element of K19( the carrier of X)
S \/ {([#] X)} is non empty set
union G is Element of K19( the carrier of (X))
P is set
(U `) \/ U is Element of K19( the carrier of X)
union Vx is Element of K19( the carrier of X)
union c12 is Element of K19( the carrier of (X))
z is set
S is set
Z is Element of K19( the carrier of X)
Z \/ {([#] X)} is non empty set
union {Q} is Element of K19( the carrier of (X))
(union c12) \/ () is Element of K19( the carrier of (X))
X is non empty TopSpace-like TopStruct
(X) is non empty strict TopSpace-like compact () TopStruct
the carrier of X is non empty set
K19( the carrier of X) is non empty V21() V23() V24() set
[#] X is non empty non proper open closed dense non boundary Element of K19( the carrier of X)
{([#] X)} is non empty finite Element of K19(K19( the carrier of X))
K19(K19( the carrier of X)) is non empty V21() V23() V24() set
{ (b1 \/ {([#] X)}) where b1 is Element of K19( the carrier of X) : ( b1 is open & b1 ` is compact ) } is set
[#] (X) is non empty non proper open closed dense non boundary compact Element of K19( the carrier of (X))
the carrier of (X) is non empty set
K19( the carrier of (X)) is non empty V21() V23() V24() set
succ ([#] X) is set
{([#] X)} is non empty finite set
([#] X) \/ {([#] X)} is non empty set
the topology of (X) is non empty open Element of K19(K19( the carrier of (X)))
K19(K19( the carrier of (X))) is non empty V21() V23() V24() set
the topology of X is non empty open Element of K19(K19( the carrier of X))
the topology of X \/ { (b1 \/ {([#] X)}) where b1 is Element of K19( the carrier of X) : ( b1 is open & b1 ` is compact ) } is non empty set
Xy is Element of the carrier of (X)
x is Element of the carrier of (X)
P is Element of K19( the carrier of X)
Q is Element of K19( the carrier of X)
Vx is Element of K19( the carrier of (X))
U is Element of K19( the carrier of (X))
P is Element of the carrier of X
Q is a_neighborhood of P
Int Q is open Element of K19( the carrier of X)
Q ` is Element of K19( the carrier of X)
the carrier of X \ Q is set
Cl (Q `) is closed Element of K19( the carrier of X)
(Cl (Q `)) ` is open Element of K19( the carrier of X)
the carrier of X \ (Cl (Q `)) is set
(Q `) ` is Element of K19( the carrier of X)
the carrier of X \ (Q `) is set
(Q `) \/ {([#] X)} is non empty set
U is Element of K19( the carrier of (X))
Vx is Element of K19( the carrier of (X))
P is Element of the carrier of X
Q is a_neighborhood of P
Int Q is open Element of K19( the carrier of X)
Q ` is Element of K19( the carrier of X)
the carrier of X \ Q is set
Cl (Q `) is closed Element of K19( the carrier of X)
(Cl (Q `)) ` is open Element of K19( the carrier of X)
the carrier of X \ (Cl (Q `)) is set
(Q `) ` is Element of K19( the carrier of X)
the carrier of X \ (Q `) is set
(Q `) \/ {([#] X)} is non empty set
Vx is Element of K19( the carrier of (X))
U is Element of K19( the carrier of (X))
Xy is Element of the carrier of X
x is Element of the carrier of (X)
D is Element of the carrier of (X)
P is Element of K19( the carrier of (X))
Q is Element of K19( the carrier of (X))
U is Element of K19( the carrier of X)
U \/ {([#] X)} is non empty set
U ` is Element of K19( the carrier of X)
the carrier of X \ U is set
([#] X) \ Q is Element of K19( the carrier of X)
([#] X) \ U is Element of K19( the carrier of X)
([#] X) \ {([#] X)} is Element of K19( the carrier of X)
(([#] X) \ U) /\ (([#] X) \ {([#] X)}) is Element of K19( the carrier of X)
(([#] X) \ U) /\ ([#] X) is Element of K19( the carrier of X)
([#] (X)) \ Q is Element of K19( the carrier of (X))
{([#] X)} \ Q is finite Element of K19(K19( the carrier of X))
(([#] X) \ Q) \/ ({([#] X)} \ Q) is set
(([#] X) \ U) \/ {} is set
Q ` is Element of K19( the carrier of (X))
the carrier of (X) \ Q is set
Vx is Element of K19( the carrier of X)
Vx \/ {([#] X)} is non empty set
Vx ` is Element of K19( the carrier of X)
the carrier of X \ Vx is set
Vx is open Element of K19( the carrier of X)
Cl Vx is closed Element of K19( the carrier of X)
Int Vx is open Element of K19( the carrier of X)
Vx ` is closed Element of K19( the carrier of X)
the carrier of X \ Vx is set
Cl (Vx `) is closed Element of K19( the carrier of X)
(Cl (Vx `)) ` is open Element of K19( the carrier of X)
the carrier of X \ (Cl (Vx `)) is set
Int (Cl Vx) is open Element of K19( the carrier of X)
(Cl Vx) ` is open Element of K19( the carrier of X)
the carrier of X \ (Cl Vx) is set
Cl ((Cl Vx) `) is closed Element of K19( the carrier of X)
(Cl ((Cl Vx) `)) ` is open Element of K19( the carrier of X)
the carrier of X \ (Cl ((Cl Vx) `)) is set
K is a_neighborhood of Xy
(Q `) /\ ([#] X) is Element of K19( the carrier of X)
X is non empty TopSpace-like TopStruct
(X) is non empty strict TopSpace-like compact () TopStruct
the carrier of (X) is non empty set
K19( the carrier of (X)) is non empty V21() V23() V24() set
[#] X is non empty non proper open closed dense non boundary Element of K19( the carrier of X)
the carrier of X is non empty set
K19( the carrier of X) is non empty V21() V23() V24() set
{([#] X)} is non empty finite Element of K19(K19( the carrier of X))
K19(K19( the carrier of X)) is non empty V21() V23() V24() set
{ (b1 \/ {([#] X)}) where b1 is Element of K19( the carrier of X) : ( b1 is open & b1 ` is compact ) } is set
[#] (X) is non empty non proper open closed dense non boundary compact Element of K19( the carrier of (X))
succ ([#] X) is set
{([#] X)} is non empty finite set
([#] X) \/ {([#] X)} is non empty set
the topology of (X) is non empty open Element of K19(K19( the carrier of (X)))
K19(K19( the carrier of (X))) is non empty V21() V23() V24() set
the topology of X is non empty open Element of K19(K19( the carrier of X))
the topology of X \/ { (b1 \/ {([#] X)}) where b1 is Element of K19( the carrier of X) : ( b1 is open & b1 ` is compact ) } is non empty set
D is Element of K19( the carrier of (X))
Cl D is closed Element of K19( the carrier of (X))
Xy is Element of the carrier of (X)
{Xy} is non empty finite compact Element of K19( the carrier of (X))
x is Element of K19( the carrier of (X))
([#] (X)) \ (Cl D) is Element of K19( the carrier of (X))
([#] X) \ (Cl D) is Element of K19( the carrier of X)
{([#] X)} \ (Cl D) is finite Element of K19(K19( the carrier of X))
(([#] X) \ (Cl D)) \/ ({([#] X)} \ (Cl D)) is set
{} \/ ({([#] X)} \ (Cl D)) is finite set
P is Element of K19( the carrier of X)
P \/ {([#] X)} is non empty set
P ` is Element of K19( the carrier of X)
the carrier of X \ P is set

(Cl D) \/ {([#] X)} is non empty set
D is Element of K19( the carrier of (X))
Cl D is closed Element of K19( the carrier of (X))

({} X) ` is open closed dense Element of K19( the carrier of X)
the carrier of X \ ({} X) is set
({} X) \/ {([#] X)} is non empty finite set
Xy is Element of K19( the carrier of (X))
Xy ` is Element of K19( the carrier of (X))
the carrier of (X) \ Xy is set
Cl (Xy `) is closed Element of K19( the carrier of (X))
([#] X) \ Xy is Element of K19( the carrier of X)
X is non empty TopSpace-like TopStruct
(X) is non empty strict TopSpace-like compact () TopStruct
incl (X,(X)) is Relation-like the carrier of X -defined the carrier of (X) -valued Function-like V18( the carrier of X, the carrier of (X)) Element of K19(K20( the carrier of X, the carrier of (X)))
the carrier of X is non empty set
the carrier of (X) is non empty set
K20( the carrier of X, the carrier of (X)) is Relation-like non empty set
K19(K20( the carrier of X, the carrier of (X))) is non empty V21() V23() V24() set
K19( the carrier of X) is non empty V21() V23() V24() set
[#] X is non empty non proper open closed dense non boundary Element of K19( the carrier of X)
{([#] X)} is non empty finite Element of K19(K19( the carrier of X))
K19(K19( the carrier of X)) is non empty V21() V23() V24() set
{ (b1 \/ {([#] X)}) where b1 is Element of K19( the carrier of X) : ( b1 is open & b1 ` is compact ) } is set
K19( the carrier of (X)) is non empty V21() V23() V24() set
[#] (X) is non empty non proper open closed dense non boundary compact Element of K19( the carrier of (X))
Xy is Element of K19( the carrier of (X))
(X) | Xy is strict TopSpace-like SubSpace of (X)
[#] ((X) | Xy) is non proper open closed dense Element of K19( the carrier of ((X) | Xy))
the carrier of ((X) | Xy) is set
K19( the carrier of ((X) | Xy)) is non empty V21() V23() V24() set
the topology of (X) is non empty open Element of K19(K19( the carrier of (X)))
K19(K19( the carrier of (X))) is non empty V21() V23() V24() set
the topology of X is non empty open Element of K19(K19( the carrier of X))
the topology of X \/ { (b1 \/ {([#] X)}) where b1 is Element of K19( the carrier of X) : ( b1 is open & b1 ` is compact ) } is non empty set
the topology of ((X) | Xy) is non empty open Element of K19(K19( the carrier of ((X) | Xy)))
K19(K19( the carrier of ((X) | Xy))) is non empty V21() V23() V24() set
x is set
P is Element of K19( the carrier of ((X) | Xy))
Q is Element of K19( the carrier of (X))
Q /\ ([#] ((X) | Xy)) is Element of K19( the carrier of ((X) | Xy))
U is Element of K19( the carrier of X)
U \/ {([#] X)} is non empty set
U ` is Element of K19( the carrier of X)
the carrier of X \ U is set
{([#] X)} /\ ([#] X) is finite compact Element of K19( the carrier of X)
U /\ ([#] X) is Element of K19( the carrier of X)
(U /\ ([#] X)) \/ {} is set
x is set
P is Element of K19( the carrier of ((X) | Xy))
Q is Element of K19( the carrier of (X))
Q /\ ([#] ((X) | Xy)) is Element of K19( the carrier of ((X) | Xy))
(incl (X,(X))) .: ([#] X) is Element of K19( the carrier of (X))
x is Element of K19( the carrier of (X))