:: 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
{} is Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty finite finite-yielding V36() set
the Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty finite finite-yielding V36() set is Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty finite finite-yielding V36() set
1 is non empty set
X is TopSpace-like TopStruct
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
X is TopSpace-like TopStruct
the carrier of X is set
K19( the carrier of X) is non empty V21() V23() V24() set
X is TopSpace-like TopStruct
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)
X is TopSpace-like TopStruct
the carrier of X is set
K19( the carrier of X) is non empty V21() V23() V24() set
{} X is Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty finite finite-yielding V36() open closed boundary nowhere_dense compact (X) Element of K19( the carrier of X)
X is TopSpace-like TopStruct
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)
X is TopSpace-like TopStruct
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
{ b₁ where b₁ is a_neighborhood of h : ( b₁ is compact & ex b₂ being a_neighborhood of h st b₁ c= b₂ ) } 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
{ b₁ where b₁ is a_neighborhood of h : ( b₁ is compact & ex b₂, b₃ being a_neighborhood of h st b₁ c= b₂ /\ b₃ ) } 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
the non empty TopSpace-like T_0 T_1 T_2 regular normal T_3 T_4 discrete locally-compact () () () TopStruct is non empty TopSpace-like T_0 T_1 T_2 regular normal T_3 T_4 discrete locally-compact () () () TopStruct
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
X is non empty TopSpace-like regular locally-compact () 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 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
{ b₁ where b₁ is Element of K19( the carrier of X) : ( b₁ is open & b₁ 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 { b<sub>1</sub> where b<sub>1</sub> is Element of K19( the carrier of X) : ( b<sub>1</sub> is open & b<sub>1</sub> c= h ) } is set
X is 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)
h is TopSpace-like TopStruct
[#] 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) is Relation-like [#] X -defined [#] X -valued Function-like one-to-one set
(id ([#] X)) .: D is set
X is TopSpace-like TopStruct
the carrier of X is set
h is TopSpace-like TopStruct
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 TopSpace-like 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
h is TopSpace-like TopStruct
[#] 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)))))
X is TopSpace-like TopStruct
the carrier of X is set
h is TopSpace-like TopStruct
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 TopSpace-like TopStruct
the carrier of X is set
h is TopSpace-like TopStruct
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))
{ (b<sub>1</sub> \/ {([#] X)}) where b<sub>1</sub> is Element of K19( the carrier of X) : ( b<sub>1</sub> is open & b<sub>1</sub> ` is compact ) } is set
the topology of X \/ { (b₁ \/ {([#] X)}) where b₁ is Element of K19( the carrier of X) : ( b₁ is open & b₁ ` 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
h 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
D is strict TopStruct
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 TopSpace-like TopStruct
(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
{ (b₁ \/ {([#] X)}) where b₁ is Element of K19( the carrier of X) : ( b₁ is open & b₁ ` 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 \/ { (b<sub>1</sub> \/ {([#] X)}) where b<sub>1</sub> is Element of K19( the carrier of X) : ( b<sub>1</sub> is open & b<sub>1</sub> ` 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 Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty finite finite-yielding V36() open closed boundary nowhere_dense compact (X) 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) `) ` 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)))
{ b<sub>1</sub> where b<sub>1</sub> is Element of K19( the carrier of X) : ( b<sub>1</sub> is open & ( b<sub>1</sub> in x or b<sub>1</sub> \/ {([#] 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))
(union 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)
(union Q) ` is Element of K19( the carrier of X)
the carrier of X \ (union Q) is set
(union Q) \/ {([#] X)} is non empty set
(union x) \/ {([#] 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
{ (b₁ \/ {([#] X)}) where b₁ is Element of K19( the carrier of X) : ( b₁ is open & b₁ ` 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 \/ { (b<sub>1</sub> \/ {([#] X)}) where b<sub>1</sub> is Element of K19( the carrier of X) : ( b<sub>1</sub> is open & b<sub>1</sub> ` 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 TopSpace-like TopStruct
(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
{ (b<sub>1</sub> \/ {([#] X)}) where b<sub>1</sub> is Element of K19( the carrier of X) : ( b<sub>1</sub> is open & b<sub>1</sub> ` 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))
{ b₁ where b₁ is Element of K19( the carrier of X) : ( b₁ is open & ( ( b₁ in D & not b₁ \/ {([#] X)} in D ) or b₁ \/ {([#] 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 \/ { (b₁ \/ {([#] X)}) where b₁ is Element of K19( the carrier of X) : ( b₁ is open & b₁ ` 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))
c₁₂ is Element of K19( the carrier of X)
c₁₂ \/ {([#] X)} is non empty set
union x is Element of K19( the carrier of X)
c₁₂ is Element of K19( the carrier of X)
c₁₂ \/ {([#] X)} is non empty set
c₁₂ ` is Element of K19( the carrier of X)
the carrier of X \ c<sub>12</sub> 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))
{ b<sub>1</sub> where b<sub>1</sub> is Element of K19( the carrier of (X)) : ( b<sub>1</sub> in D & ex b<sub>2</sub> being Element of K19( the carrier of X) st
( b<sub>2</sub> in Vx & ( ( b<sub>2</sub> in D & not b<sub>2</sub> \/ {([#] X)} in D & b<sub>1</sub> = b<sub>2</sub> ) or ( b<sub>2</sub> \/ {([#] X)} in D & b<sub>1</sub> = b<sub>2</sub> \/ {([#] X)} ) ) ) ) } is set
K is set
c<sub>12</sub> is Element of K19( the carrier of (X))
K is set
K \/ {([#] X)} is non empty set
c<sub>12</sub> is Element of K19( the carrier of X)
c<sub>12</sub> \/ {([#] X)} is non empty set
G is Element of K19( the carrier of (X))
G is Element of K19( the carrier of (X))
K is Relation-like Function-like set
dom K is set
rng K is set
c<sub>12</sub> 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
c<sub>12</sub> is finite Element of K19(K19( the carrier of (X)))
{Q} is non empty finite Element of K19(K19( the carrier of (X)))
c<sub>12</sub> \/ {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 c₁₂ 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 c₁₂) \/ (union {Q}) 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
{ (b₁ \/ {([#] X)}) where b₁ is Element of K19( the carrier of X) : ( b₁ is open & b₁ ` 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 \/ { (b<sub>1</sub> \/ {([#] X)}) where b<sub>1</sub> is Element of K19( the carrier of X) : ( b<sub>1</sub> is open & b<sub>1</sub> ` 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
{ (b₁ \/ {([#] X)}) where b₁ is Element of K19( the carrier of X) : ( b₁ is open & b₁ ` 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 \/ { (b<sub>1</sub> \/ {([#] X)}) where b<sub>1</sub> is Element of K19( the carrier of X) : ( b<sub>1</sub> is open & b<sub>1</sub> ` 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
{} X is Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty proper finite finite-yielding V36() open closed boundary nowhere_dense compact (X) Element of K19( the carrier of X)
(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 Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty proper finite finite-yielding V36() open closed boundary nowhere_dense compact (X) 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
{ (b₁ \/ {([#] X)}) where b₁ is Element of K19( the carrier of X) : ( b₁ is open & b₁ ` 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 \/ { (b<sub>1</sub> \/ {([#] X)}) where b<sub>1</sub> is Element of K19( the carrier of X) : ( b<sub>1</sub> is open & b<sub>1</sub> ` 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))