:: CONNSP_2 semantic presentation

K121() is set

K10(K121()) is non empty set

{} is empty set

1 is non empty set

X is non empty TopSpace-like TopStruct

the U1 of X is non empty set

K10( the U1 of X) is non empty set

A is Element of the U1 of X

[#] X is non empty non proper open closed dense non boundary Element of K10( the U1 of X)

Int ([#] X) is open Element of K10( the U1 of X)

X is TopSpace-like TopStruct

the U1 of X is set

K10( the U1 of X) is non empty set

A is Element of K10( the U1 of X)

[#] X is non proper open closed dense Element of K10( the U1 of X)

Int ([#] X) is open Element of K10( the U1 of X)

X is non empty TopSpace-like TopStruct

the U1 of X is non empty set

K10( the U1 of X) is non empty set

A is Element of the U1 of X

Y is Element of K10( the U1 of X)

G is Element of K10( the U1 of X)

Y \/ G is Element of K10( the U1 of X)

B1 is Element of K10( the U1 of X)

B is Element of K10( the U1 of X)

B1 \/ B is Element of K10( the U1 of X)

Int B1 is open Element of K10( the U1 of X)

Int B is open Element of K10( the U1 of X)

(Int B1) \/ (Int B) is open Element of K10( the U1 of X)

Int (B1 \/ B) is open Element of K10( the U1 of X)

X is non empty TopSpace-like TopStruct

the U1 of X is non empty set

K10( the U1 of X) is non empty set

A is Element of the U1 of X

Y is Element of K10( the U1 of X)

G is Element of K10( the U1 of X)

Y /\ G is Element of K10( the U1 of X)

Int Y is open Element of K10( the U1 of X)

Int G is open Element of K10( the U1 of X)

(Int Y) /\ (Int G) is open Element of K10( the U1 of X)

Int (Y /\ G) is open Element of K10( the U1 of X)

X is non empty TopSpace-like TopStruct

the U1 of X is non empty set

K10( the U1 of X) is non empty set

A is Element of K10( the U1 of X)

Y is Element of the U1 of X

Int A is open Element of K10( the U1 of X)

X is non empty TopSpace-like TopStruct

the U1 of X is non empty set

K10( the U1 of X) is non empty set

A is Element of K10( the U1 of X)

Y is Element of the U1 of X

Int A is open Element of K10( the U1 of X)

X is non empty TopSpace-like TopStruct

the U1 of X is non empty set

K10( the U1 of X) is non empty set

A is Element of the U1 of X

Y is Element of K10( the U1 of X)

Int Y is open Element of K10( the U1 of X)

G is Element of K10( the U1 of X)

B1 is non empty Element of K10( the U1 of X)

X is non empty TopSpace-like TopStruct

the U1 of X is non empty set

K10( the U1 of X) is non empty set

A is Element of the U1 of X

Y is Element of K10( the U1 of X)

G is non empty Element of K10( the U1 of X)

G is Element of K10( the U1 of X)

Int Y is open Element of K10( the U1 of X)

G is Element of K10( the U1 of X)

B is Element of K10( the U1 of X)

X is non empty TopSpace-like TopStruct

the U1 of X is non empty set

K10( the U1 of X) is non empty set

A is Element of K10( the U1 of X)

Y is set

G is Element of the U1 of X

B1 is Element of K10( the U1 of X)

B is Element of K10( the U1 of X)

G is Element of K10( the U1 of X)

Y is Element of the U1 of X

G is Element of the U1 of X

X is non empty TopSpace-like TopStruct

the U1 of X is non empty set

K10( the U1 of X) is non empty set

A is Element of the U1 of X

{A} is non empty connected Element of K10( the U1 of X)

Y is Element of K10( the U1 of X)

Int Y is open Element of K10( the U1 of X)

Int Y is open Element of K10( the U1 of X)

G is set

X is non empty TopSpace-like TopStruct

the U1 of X is non empty set

K10( the U1 of X) is non empty set

A is non empty Element of K10( the U1 of X)

X | A is non empty strict TopSpace-like SubSpace of X

the U1 of (X | A) is non empty set

K10( the U1 of (X | A)) is non empty set

Y is Element of the U1 of (X | A)

G is Element of K10( the U1 of (X | A))

B1 is Element of K10( the U1 of X)

B is Element of the U1 of X

Int G is open Element of K10( the U1 of (X | A))

y is Element of K10( the U1 of (X | A))

the topology of (X | A) is non empty Element of K10(K10( the U1 of (X | A)))

K10(K10( the U1 of (X | A))) is non empty set

the topology of X is non empty Element of K10(K10( the U1 of X))

K10(K10( the U1 of X)) is non empty set

[#] (X | A) is non empty non proper open closed dense non boundary Element of K10( the U1 of (X | A))

B is Element of K10( the U1 of X)

B /\ ([#] (X | A)) is Element of K10( the U1 of (X | A))

B1 is Element of K10( the U1 of X)

B /\ A is Element of K10( the U1 of X)

Int B1 is open Element of K10( the U1 of X)

X is non empty TopSpace-like TopStruct

the U1 of X is non empty set

K10( the U1 of X) is non empty set

A is TopSpace-like SubSpace of X

the U1 of A is set

K10( the U1 of A) is non empty set

[#] A is non proper open closed dense Element of K10( the U1 of A)

Y is Element of K10( the U1 of X)

Int Y is open Element of K10( the U1 of X)

(Int Y) /\ ([#] A) is Element of K10( the U1 of A)

G is Element of K10( the U1 of A)

Int G is open Element of K10( the U1 of A)

B1 is set

B is Element of K10( the U1 of X)

B /\ ([#] A) is Element of K10( the U1 of A)

y is Element of K10( the U1 of A)

the topology of X is non empty Element of K10(K10( the U1 of X))

K10(K10( the U1 of X)) is non empty set

the topology of A is non empty Element of K10(K10( the U1 of A))

K10(K10( the U1 of A)) is non empty set

y is Element of K10( the U1 of A)

X is non empty TopSpace-like TopStruct

the U1 of X is non empty set

K10( the U1 of X) is non empty set

A is non empty Element of K10( the U1 of X)

X | A is non empty strict TopSpace-like SubSpace of X

the U1 of (X | A) is non empty set

K10( the U1 of (X | A)) is non empty set

Y is Element of the U1 of (X | A)

G is Element of K10( the U1 of (X | A))

B1 is Element of K10( the U1 of X)

B is Element of the U1 of X

Int B1 is open Element of K10( the U1 of X)

[#] (X | A) is non empty non proper open closed dense non boundary Element of K10( the U1 of (X | A))

(Int B1) /\ ([#] (X | A)) is Element of K10( the U1 of (X | A))

Int G is open Element of K10( the U1 of (X | A))

X is non empty TopSpace-like TopStruct

the U1 of X is non empty set

K10( the U1 of X) is non empty set

A is Element of K10( the U1 of X)

Y is Element of K10( the U1 of X)

X | Y is strict TopSpace-like SubSpace of X

the U1 of (X | Y) is set

K10( the U1 of (X | Y)) is non empty set

[#] (X | Y) is non proper open closed dense Element of K10( the U1 of (X | Y))

G is Element of K10( the U1 of (X | Y))

B1 is Element of K10( the U1 of (X | Y))

B is Element of K10( the U1 of (X | Y))

y is Element of K10( the U1 of X)

G is Element of K10( the U1 of (X | Y))

X is non empty TopSpace-like TopStruct

the U1 of X is non empty set

A is non empty TopSpace-like SubSpace of X

the U1 of A is non empty set

Y is Element of the U1 of X

Component_of Y is non empty connected Element of K10( the U1 of X)

K10( the U1 of X) is non empty set

G is Element of the U1 of A

Component_of G is non empty connected Element of K10( the U1 of A)

K10( the U1 of A) is non empty set

K10(K10( the U1 of X)) is non empty set

B1 is Element of K10(K10( the U1 of X))

union B1 is Element of K10( the U1 of X)

B is Element of K10( the U1 of X)

X is non empty TopSpace-like TopStruct

the U1 of X is non empty set

X is non empty TopSpace-like TopStruct

the U1 of X is non empty set

K10( the U1 of X) is non empty set

X is non empty TopSpace-like TopStruct

the U1 of X is non empty set

K10( the U1 of X) is non empty set

X is non empty TopSpace-like TopStruct

the U1 of X is non empty set

K10( the U1 of X) is non empty set

A is Element of the U1 of X

Y is Element of K10( the U1 of X)

G is Element of K10( the U1 of X)

X | Y is strict TopSpace-like SubSpace of X

the U1 of (X | Y) is set

K10( the U1 of (X | Y)) is non empty set

B is Element of K10( the U1 of (X | Y))

y is Element of K10( the U1 of X)

[#] (X | Y) is non proper open closed dense Element of K10( the U1 of (X | Y))

Int y is open Element of K10( the U1 of X)

B is Element of K10( the U1 of (X | Y))

B /\ B is Element of K10( the U1 of (X | Y))

B1 is non empty Element of K10( the U1 of X)

X | B1 is non empty strict TopSpace-like SubSpace of X

{} (X | B1) is empty proper open closed boundary nowhere_dense connected Element of K10( the U1 of (X | B1))

the U1 of (X | B1) is non empty set

K10( the U1 of (X | B1)) is non empty set

Int G is open Element of K10( the U1 of X)

Y is Element of K10( the U1 of X)

X | Y is strict TopSpace-like SubSpace of X

[#] (X | Y) is non proper open closed dense Element of K10( the U1 of (X | Y))

the U1 of (X | Y) is set

K10( the U1 of (X | Y)) is non empty set

G is non empty Element of K10( the U1 of X)

X | G is non empty strict TopSpace-like SubSpace of X

[#] (X | G) is non empty non proper open closed dense non boundary Element of K10( the U1 of (X | G))

the U1 of (X | G) is non empty set

K10( the U1 of (X | G)) is non empty set

B1 is Element of the U1 of (X | G)

Component_of B1 is non empty connected Element of K10( the U1 of (X | G))

y is Element of K10( the U1 of X)

X is non empty TopSpace-like TopStruct

the U1 of X is non empty set

K10( the U1 of X) is non empty set

A is Element of the U1 of X

Y is non empty Element of K10( the U1 of X)

X | Y is non empty strict TopSpace-like SubSpace of X

the U1 of (X | Y) is non empty set

[#] (X | Y) is non empty non proper open closed dense non boundary Element of K10( the U1 of (X | Y))

K10( the U1 of (X | Y)) is non empty set

G is Element of the U1 of (X | Y)

Component_of G is non empty connected Element of K10( the U1 of (X | Y))

Int (Component_of G) is open Element of K10( the U1 of (X | Y))

B1 is Element of K10( the U1 of (X | Y))

B is Element of K10( the U1 of X)

Y is Element of K10( the U1 of X)

G is non empty Element of K10( the U1 of X)

X | G is non empty strict TopSpace-like SubSpace of X

the U1 of (X | G) is non empty set

B1 is Element of the U1 of (X | G)

Component_of B1 is non empty connected Element of K10( the U1 of (X | G))

K10( the U1 of (X | G)) is non empty set

Int (Component_of B1) is open Element of K10( the U1 of (X | G))

y is Element of K10( the U1 of X)

[#] (X | G) is non empty non proper open closed dense non boundary Element of K10( the U1 of (X | G))

Y is non empty Element of K10( the U1 of X)

X | Y is non empty strict TopSpace-like SubSpace of X

the U1 of (X | Y) is non empty set

G is non empty Element of K10( the U1 of X)

X | G is non empty strict TopSpace-like SubSpace of X

the U1 of (X | G) is non empty set

X is non empty TopSpace-like TopStruct

the U1 of X is non empty set

K10( the U1 of X) is non empty set

A is Element of K10( the U1 of X)

Y is set

[#] X is non empty non proper open closed dense non boundary Element of K10( the U1 of X)

G is Element of the U1 of X

Int A is open Element of K10( the U1 of X)

X is non empty TopSpace-like TopStruct

the U1 of X is non empty set

K10( the U1 of X) is non empty set

A is Element of the U1 of X

Y is non empty Element of K10( the U1 of X)

X | Y is non empty strict TopSpace-like SubSpace of X

[#] (X | Y) is non empty non proper open closed dense non boundary Element of K10( the U1 of (X | Y))

the U1 of (X | Y) is non empty set

K10( the U1 of (X | Y)) is non empty set

G is non empty Element of K10( the U1 of X)

B1 is non empty Element of K10( the U1 of X)

X | B1 is non empty strict TopSpace-like SubSpace of X

the U1 of (X | B1) is non empty set

B is Element of the U1 of (X | B1)

y is Element of the U1 of (X | B1)

X | G is non empty strict TopSpace-like SubSpace of X

the U1 of (X | G) is non empty set

K10( the U1 of (X | G)) is non empty set

B is Element of K10( the U1 of (X | G))

B1 is Element of K10( the U1 of X)

R is Element of K10( the U1 of X)

A1 is Element of K10( the U1 of (X | G))

X is non empty TopSpace-like TopStruct

the U1 of X is non empty set

K10( the U1 of X) is non empty set

A is non empty Element of K10( the U1 of X)

X | A is non empty strict TopSpace-like SubSpace of X

the U1 of (X | A) is non empty set

Y is Element of the U1 of (X | A)

[#] (X | A) is non empty non proper open closed dense non boundary Element of K10( the U1 of (X | A))

K10( the U1 of (X | A)) is non empty set

G is Element of the U1 of X

B1 is Element of the U1 of (X | A)

X is non empty TopSpace-like TopStruct

the U1 of X is non empty set

K10( the U1 of X) is non empty set

A is non empty Element of K10( the U1 of X)

Y is Element of K10( the U1 of X)

X | A is non empty strict TopSpace-like SubSpace of X

the U1 of (X | A) is non empty set

K10( the U1 of (X | A)) is non empty set

G is Element of K10( the U1 of (X | A))

B1 is Element of K10( the U1 of (X | A))

the topology of (X | A) is non empty Element of K10(K10( the U1 of (X | A)))

K10(K10( the U1 of (X | A))) is non empty set

the topology of X is non empty Element of K10(K10( the U1 of X))

K10(K10( the U1 of X)) is non empty set

[#] (X | A) is non empty non proper open closed dense non boundary Element of K10( the U1 of (X | A))

B is Element of K10( the U1 of X)

B /\ ([#] (X | A)) is Element of K10( the U1 of (X | A))

B /\ A is Element of K10( the U1 of X)

y is Element of K10( the U1 of X)

A is Element of the U1 of X

Y is non empty Element of K10( the U1 of X)

X | Y is non empty strict TopSpace-like SubSpace of X

the U1 of (X | Y) is non empty set

[#] (X | Y) is non empty non proper open closed dense non boundary Element of K10( the U1 of (X | Y))

K10( the U1 of (X | Y)) is non empty set

G is Element of the U1 of (X | Y)

Component_of G is non empty connected Element of K10( the U1 of (X | Y))

B is Element of K10( the U1 of X)

Int (Component_of G) is open Element of K10( the U1 of (X | Y))

X is non empty TopSpace-like TopStruct

the U1 of X is non empty set

K10( the U1 of X) is non empty set

A is non empty Element of K10( the U1 of X)

X | A is non empty strict TopSpace-like SubSpace of X

the U1 of (X | A) is non empty set

K10( the U1 of (X | A)) is non empty set

Y is non empty Element of K10( the U1 of (X | A))

the topology of (X | A) is non empty Element of K10(K10( the U1 of (X | A)))

K10(K10( the U1 of (X | A))) is non empty set

the topology of X is non empty Element of K10(K10( the U1 of X))

K10(K10( the U1 of X)) is non empty set

[#] (X | A) is non empty non proper open closed dense non boundary Element of K10( the U1 of (X | A))

G is Element of K10( the U1 of X)

G /\ ([#] (X | A)) is Element of K10( the U1 of (X | A))

G /\ A is Element of K10( the U1 of X)

B1 is non empty Element of K10( the U1 of X)

{} (X | A) is empty proper open closed boundary nowhere_dense connected Element of K10( the U1 of (X | A))

y is Element of the U1 of (X | A)

X | B1 is non empty strict TopSpace-like SubSpace of X

[#] (X | B1) is non empty non proper open closed dense non boundary Element of K10( the U1 of (X | B1))

the U1 of (X | B1) is non empty set

K10( the U1 of (X | B1)) is non empty set

B is Element of the U1 of (X | B1)

Component_of B is non empty connected Element of K10( the U1 of (X | B1))

R is Element of K10( the U1 of X)

A /\ R is Element of K10( the U1 of X)

B is Element of K10( the U1 of X)

A1 is Element of K10( the U1 of (X | B1))

A1 /\ R is Element of K10( the U1 of X)

{} (X | B1) is empty proper open closed boundary nowhere_dense connected Element of K10( the U1 of (X | B1))

B1 /\ A is Element of K10( the U1 of X)

R /\ (B1 /\ A) is Element of K10( the U1 of X)

R /\ B1 is Element of K10( the U1 of X)

(R /\ B1) /\ A is Element of K10( the U1 of X)

X is non empty TopSpace-like TopStruct

the U1 of X is non empty set

K10( the U1 of X) is non empty set

[#] X is non empty non proper open closed dense non boundary Element of K10( the U1 of X)

A is Element of K10( the U1 of X)

Y is Element of K10( the U1 of X)

([#] X) \ Y is Element of K10( the U1 of X)

A ` is Element of K10( the U1 of X)

the U1 of X \ A is set

Y ` is Element of K10( the U1 of X)

the U1 of X \ Y is set

B1 is Element of K10( the U1 of X)

B is Element of K10( the U1 of X)

Cl B1 is closed Element of K10( the U1 of X)

y is set

B ` is Element of K10( the U1 of X)

the U1 of X \ B is set

B is Element of the U1 of X

(([#] X) \ Y) ` is Element of K10( the U1 of X)

the U1 of X \ (([#] X) \ Y) is set

A is Element of K10( the U1 of X)

Y is Element of K10( the U1 of X)

([#] X) \ Y is Element of K10( the U1 of X)

([#] X) \ (([#] X) \ Y) is Element of K10( the U1 of X)

Y ` is Element of K10( the U1 of X)

the U1 of X \ Y is set

B1 is Element of K10( the U1 of X)

Cl B1 is closed Element of K10( the U1 of X)

([#] X) \ (Cl B1) is Element of K10( the U1 of X)

B is Element of K10( the U1 of X)

(([#] X) \ Y) ` is Element of K10( the U1 of X)

the U1 of X \ (([#] X) \ Y) is set

(Cl B1) ` is open Element of K10( the U1 of X)

the U1 of X \ (Cl B1) is set

B1 ` is Element of K10( the U1 of X)

the U1 of X \ B1 is set

X is non empty TopSpace-like TopStruct

the U1 of X is non empty set

K10( the U1 of X) is non empty set

A is Element of K10( the U1 of X)

Y is Element of K10( the U1 of X)

[#] X is non empty non proper open closed dense non boundary Element of K10( the U1 of X)

([#] X) \ Y is Element of K10( the U1 of X)

([#] X) \ (([#] X) \ Y) is Element of K10( the U1 of X)

{} X is empty proper open closed boundary nowhere_dense connected Element of K10( the U1 of X)

G is Element of the U1 of X

Y ` is Element of K10( the U1 of X)

the U1 of X \ Y is set

B1 is Element of K10( the U1 of X)

Cl B1 is closed Element of K10( the U1 of X)

B is non empty Element of K10( the U1 of X)

X | B is non empty strict TopSpace-like SubSpace of X

[#] (X | B) is non empty non proper open closed dense non boundary Element of K10( the U1 of (X | B))

the U1 of (X | B) is non empty set

K10( the U1 of (X | B)) is non empty set

Cl B is closed Element of K10( the U1 of X)

(Cl B) ` is open Element of K10( the U1 of X)

the U1 of X \ (Cl B) is set

y is Element of the U1 of (X | B)

Component_of y is non empty connected Element of K10( the U1 of (X | B))

B1 is Element of K10( the U1 of X)

R is Element of K10( the U1 of X)

A1 is Element of K10( the U1 of (X | B))

A1 /\ (Component_of y) is Element of K10( the U1 of (X | B))

z is Element of the U1 of X

C is non empty Element of K10( the U1 of X)

X | C is non empty strict TopSpace-like SubSpace of X

[#] (X | C) is non empty non proper open closed dense non boundary Element of K10( the U1 of (X | C))

the U1 of (X | C) is non empty set

K10( the U1 of (X | C)) is non empty set

z1 is Element of the U1 of (X | C)

Component_of z1 is non empty connected Element of K10( the U1 of (X | C))

V1 is Element of K10( the U1 of X)

S is Element of K10( the U1 of X)

X | ((Cl B) `) is strict TopSpace-like SubSpace of X

[#] (X | ((Cl B) `)) is non proper open closed dense Element of K10( the U1 of (X | ((Cl B) `)))

the U1 of (X | ((Cl B) `)) is set

K10( the U1 of (X | ((Cl B) `))) is non empty set

B1 is Element of K10( the U1 of (X | ((Cl B) `)))

B1 /\ (Component_of z1) is Element of K10( the U1 of (X | C))

R /\ S is Element of K10( the U1 of X)

(Cl B) /\ ((Cl B) `) is Element of K10( the U1 of X)

X is non empty TopSpace-like TopStruct

the U1 of X is non empty set

K10( the U1 of X) is non empty set

K10(K10( the U1 of X)) is non empty set

[#] X is non empty non proper open closed dense non boundary Element of K10( the U1 of X)

A is Element of the U1 of X

Y is Element of K10(K10( the U1 of X))

X is non empty TopSpace-like TopStruct

the U1 of X is non empty set

K10( the U1 of X) is non empty set

K10(K10( the U1 of X)) is non empty set

A is Element of the U1 of X

Y is Element of K10(K10( the U1 of X))

meet Y is Element of K10( the U1 of X)

G is Element of K10( the U1 of X)

B1 is Element of K10( the U1 of X)

B is Element of K10( the U1 of X)

Y is Element of K10( the U1 of X)

G is Element of K10( the U1 of X)

B1 is Element of K10(K10( the U1 of X))

meet B1 is Element of K10( the U1 of X)

B1 is Element of K10(K10( the U1 of X))

meet B1 is Element of K10( the U1 of X)

B is Element of K10(K10( the U1 of X))

meet B is Element of K10( the U1 of X)

B is Element of K10(K10( the U1 of X))

meet B is Element of K10( the U1 of X)

y is set

B is set

B1 is Element of K10( the U1 of X)

B is set

B1 is Element of K10( the U1 of X)

X is non empty TopSpace-like TopStruct

the U1 of X is non empty set

A is Element of the U1 of X

(X,A) is Element of K10( the U1 of X)

K10( the U1 of X) is non empty set

K10(K10( the U1 of X)) is non empty set

Y is Element of K10(K10( the U1 of X))

meet Y is Element of K10( the U1 of X)

G is set

X is non empty TopSpace-like TopStruct

the U1 of X is non empty set

K10( the U1 of X) is non empty set

A is Element of the U1 of X

(X,A) is Element of K10( the U1 of X)

Y is Element of K10( the U1 of X)

K10(K10( the U1 of X)) is non empty set

G is Element of K10(K10( the U1 of X))

meet G is Element of K10( the U1 of X)

X is non empty TopSpace-like TopStruct

the U1 of X is non empty set

A is Element of the U1 of X

(X,A) is Element of K10( the U1 of X)

K10( the U1 of X) is non empty set

K10(K10( the U1 of X)) is non empty set

Y is Element of K10(K10( the U1 of X))

meet Y is Element of K10( the U1 of X)

G is Element of K10( the U1 of X)

X is non empty TopSpace-like TopStruct

the U1 of X is non empty set

A is Element of the U1 of X

Component_of A is non empty connected Element of K10( the U1 of X)

K10( the U1 of X) is non empty set

(X,A) is Element of K10( the U1 of X)

K10(K10( the U1 of X)) is non empty set

Y is Element of K10(K10( the U1 of X))

meet Y is Element of K10( the U1 of X)

B1 is set

B is Element of K10( the U1 of X)

B ` is Element of K10( the U1 of X)

the U1 of X \ B is set

Cl (B `) is closed Element of K10( the U1 of X)

(Component_of A) /\ B is Element of K10( the U1 of X)

(Component_of A) /\ (B `) is Element of K10( the U1 of X)

Cl B is closed Element of K10( the U1 of X)

[#] X is non empty non proper open closed dense non boundary Element of K10( the U1 of X)

B \/ (B `) is Element of K10( the U1 of X)

(Component_of A) /\ ([#] X) is Element of K10( the U1 of X)

((Component_of A) /\ B) \/ ((Component_of A) /\ (B `)) is Element of K10( the U1 of X)

{} X is empty proper open closed boundary nowhere_dense connected Element of K10( the U1 of X)

(B `) ` is Element of K10( the U1 of X)

the U1 of X \ (B `) is set

X is non empty TopSpace-like TopStruct

the U1 of X is non empty set

K10( the U1 of X) is non empty set

A is Element of K10( the U1 of X)

Cl A is closed Element of K10( the U1 of X)

Y is Element of the U1 of X

G is (X,Y)

Int G is open Element of K10( the U1 of X)

G is Element of K10( the U1 of X)

X is non empty TopSpace-like TopStruct

the U1 of X is non empty set

K10( the U1 of X) is non empty set

[#] X is non empty non proper open closed dense non boundary Element of K10( the U1 of X)

A is Element of K10( the U1 of X)

Int ([#] X) is open Element of K10( the U1 of X)

X is non empty TopSpace-like TopStruct

the U1 of X is non empty set

K10( the U1 of X) is non empty set

A is Element of K10( the U1 of X)

Y is (X,A)

Int Y is open Element of K10( the U1 of X)