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)