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

[#] 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

[#] 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

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

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

the topology of X \/ { (b

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

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

[#] (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

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

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

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

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

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

c

union x is Element of K19( the carrier of X)

c

c

c

the carrier of X \ c

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

( b

K is set

c

K is set

K \/ {([#] X)} is non empty set

c

c

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

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

{Q} is non empty finite Element of K19(K19( the carrier of (X)))

c

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

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

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

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

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

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

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