:: DECOMP_1 semantic presentation

K87() is set
K10(K87()) is non empty set
{} is set
the empty set is empty set
X is TopStruct
the U1 of X is set
K10( the U1 of X) is non empty set
{} X is Element of K10( the U1 of X)
Int ({} X) is empty boundary Element of K10( the U1 of X)
Cl (Int ({} X)) is Element of K10( the U1 of X)
Int (Cl (Int ({} X))) is Element of K10( the U1 of X)
X is TopStruct
the U1 of X is set
K10( the U1 of X) is non empty set
Y is Element of K10( the U1 of X)
Int Y is Element of K10( the U1 of X)
Cl (Int Y) is Element of K10( the U1 of X)
Y /\ (Cl (Int Y)) is Element of K10( the U1 of X)
Cl Y is Element of K10( the U1 of X)
Int (Cl Y) is Element of K10( the U1 of X)
Y /\ (Int (Cl Y)) is Element of K10( the U1 of X)
Int (Cl (Int Y)) is Element of K10( the U1 of X)
Y /\ (Int (Cl (Int Y))) is Element of K10( the U1 of X)
Cl (Int (Cl Y)) is Element of K10( the U1 of X)
Y /\ (Cl (Int (Cl Y))) is Element of K10( the U1 of X)
X is TopStruct
the U1 of X is set
K10( the U1 of X) is non empty set
Y is Element of K10( the U1 of X)
(X,Y) is Element of K10( the U1 of X)
Int Y is Element of K10( the U1 of X)
Cl (Int Y) is Element of K10( the U1 of X)
Y /\ (Cl (Int Y)) is Element of K10( the U1 of X)
(X,Y) is Element of K10( the U1 of X)
Cl Y is Element of K10( the U1 of X)
Int (Cl Y) is Element of K10( the U1 of X)
Y /\ (Int (Cl Y)) is Element of K10( the U1 of X)
(X,Y) \/ (X,Y) is Element of K10( the U1 of X)

the U1 of X is set
K10( the U1 of X) is non empty set
{ b1 where b1 is Element of K10( the U1 of X) : b1 is (X) } is set
K10(K10( the U1 of X)) is non empty set
{ b1 where b1 is Element of K10( the U1 of X) : S1[b1] } is set
{ b1 where b1 is Element of K10( the U1 of X) : b1 is (X) } is set
{ b1 where b1 is Element of K10( the U1 of X) : S1[b1] } is set
{ b1 where b1 is Element of K10( the U1 of X) : b1 is (X) } is set
{ b1 where b1 is Element of K10( the U1 of X) : S1[b1] } is set
{ b1 where b1 is Element of K10( the U1 of X) : b1 is (X) } is set
{ b1 where b1 is Element of K10( the U1 of X) : S1[b1] } is set
{ b1 where b1 is Element of K10( the U1 of X) : b1 is (X) } is set
{ b1 where b1 is Element of K10( the U1 of X) : S1[b1] } is set
{ b1 where b1 is Element of K10( the U1 of X) : Int b1 = (X,b1) } is set
{ b1 where b1 is Element of K10( the U1 of X) : S1[b1] } is set
{ b1 where b1 is Element of K10( the U1 of X) : Int b1 = (X,b1) } is set
{ b1 where b1 is Element of K10( the U1 of X) : S1[b1] } is set
{ b1 where b1 is Element of K10( the U1 of X) : Int b1 = (X,b1) } is set
{ b1 where b1 is Element of K10( the U1 of X) : S1[b1] } is set
{ b1 where b1 is Element of K10( the U1 of X) : Int b1 = (X,b1) } is set
{ b1 where b1 is Element of K10( the U1 of X) : S1[b1] } is set
{ b1 where b1 is Element of K10( the U1 of X) : (X,b1) = (X,b1) } is set
{ b1 where b1 is Element of K10( the U1 of X) : S1[b1] } is set
{ b1 where b1 is Element of K10( the U1 of X) : (X,b1) = (X,b1) } is set
{ b1 where b1 is Element of K10( the U1 of X) : S1[b1] } is set
{ b1 where b1 is Element of K10( the U1 of X) : (X,b1) = (X,b1) } is set
{ b1 where b1 is Element of K10( the U1 of X) : S1[b1] } is set
{ b1 where b1 is Element of K10( the U1 of X) : (X,b1) = (X,b1) } is set
{ b1 where b1 is Element of K10( the U1 of X) : S1[b1] } is set
{ b1 where b1 is Element of K10( the U1 of X) : (X,b1) = (X,b1) } is set
{ b1 where b1 is Element of K10( the U1 of X) : S1[b1] } is set
{ b1 where b1 is Element of K10( the U1 of X) : (X,b1) = (X,b1) } is set
{ b1 where b1 is Element of K10( the U1 of X) : S1[b1] } is set

the U1 of X is set
K10( the U1 of X) is non empty set
Y is Element of K10( the U1 of X)
(X,Y) is Element of K10( the U1 of X)
Int Y is open Element of K10( the U1 of X)
Cl (Int Y) is closed Element of K10( the U1 of X)
Int (Cl (Int Y)) is open Element of K10( the U1 of X)
Y /\ (Int (Cl (Int Y))) is Element of K10( the U1 of X)
(X,Y) is Element of K10( the U1 of X)
Cl Y is closed Element of K10( the U1 of X)
Int (Cl Y) is open Element of K10( the U1 of X)
Y /\ (Int (Cl Y)) is Element of K10( the U1 of X)
(X,Y) is Element of K10( the U1 of X)
Y /\ (Cl (Int Y)) is Element of K10( the U1 of X)
(X,Y) is Element of K10( the U1 of X)
Cl (Int (Cl Y)) is closed Element of K10( the U1 of X)
Y /\ (Cl (Int (Cl Y))) is Element of K10( the U1 of X)
Cl (Int (Cl (Int Y))) is closed Element of K10( the U1 of X)
Cl (Y /\ (Int (Cl Y))) is closed Element of K10( the U1 of X)
(Cl Y) /\ (Int (Cl Y)) is Element of K10( the U1 of X)
Cl ((Cl Y) /\ (Int (Cl Y))) is closed Element of K10( the U1 of X)
Cl (Cl (Int Y)) is closed Element of K10( the U1 of X)
Int (Int (Cl Y)) is open Element of K10( the U1 of X)

the U1 of X is set
K10( the U1 of X) is non empty set
Y is Element of K10( the U1 of X)
(X,Y) is Element of K10( the U1 of X)
Int Y is open Element of K10( the U1 of X)
Cl (Int Y) is closed Element of K10( the U1 of X)
Int (Cl (Int Y)) is open Element of K10( the U1 of X)
Y /\ (Int (Cl (Int Y))) is Element of K10( the U1 of X)

the U1 of X is set
K10( the U1 of X) is non empty set
Y is Element of K10( the U1 of X)
(X,Y) is Element of K10( the U1 of X)
Int Y is open Element of K10( the U1 of X)
Cl (Int Y) is closed Element of K10( the U1 of X)
Y /\ (Cl (Int Y)) is Element of K10( the U1 of X)

the U1 of X is set
K10( the U1 of X) is non empty set
Y is Element of K10( the U1 of X)
(X,Y) is Element of K10( the U1 of X)
Cl Y is closed Element of K10( the U1 of X)
Int (Cl Y) is open Element of K10( the U1 of X)
Y /\ (Int (Cl Y)) is Element of K10( the U1 of X)

the U1 of X is set
K10( the U1 of X) is non empty set
Y is Element of K10( the U1 of X)
(X,Y) is Element of K10( the U1 of X)
Cl Y is closed Element of K10( the U1 of X)
Int (Cl Y) is open Element of K10( the U1 of X)
Cl (Int (Cl Y)) is closed Element of K10( the U1 of X)
Y /\ (Cl (Int (Cl Y))) is Element of K10( the U1 of X)

the U1 of X is set
K10( the U1 of X) is non empty set
Y is Element of K10( the U1 of X)
(X,Y) is Element of K10( the U1 of X)
(X,Y) is Element of K10( the U1 of X)
Int Y is open Element of K10( the U1 of X)
Cl (Int Y) is closed Element of K10( the U1 of X)
Y /\ (Cl (Int Y)) is Element of K10( the U1 of X)
(X,Y) is Element of K10( the U1 of X)
Cl Y is closed Element of K10( the U1 of X)
Int (Cl Y) is open Element of K10( the U1 of X)
Y /\ (Int (Cl Y)) is Element of K10( the U1 of X)
(X,Y) \/ (X,Y) is Element of K10( the U1 of X)
(Cl (Int Y)) \/ (Int (Cl Y)) is Element of K10( the U1 of X)
Y /\ ((Cl (Int Y)) \/ (Int (Cl Y))) is Element of K10( the U1 of X)

the U1 of X is set
K10( the U1 of X) is non empty set
(X) is Element of K10(K10( the U1 of X))
K10(K10( the U1 of X)) is non empty set
{ b1 where b1 is Element of K10( the U1 of X) : b1 is (X) } is set
(X) is Element of K10(K10( the U1 of X))
{ b1 where b1 is Element of K10( the U1 of X) : Int b1 = (X,b1) } is set
(X) /\ (X) is Element of K10(K10( the U1 of X))
the topology of X is non empty Element of K10(K10( the U1 of X))
Y is set
f is Element of K10( the U1 of X)
V is Element of K10( the U1 of X)
Int V is open Element of K10( the U1 of X)
(X,V) is Element of K10( the U1 of X)
Cl (Int V) is closed Element of K10( the U1 of X)
Int (Cl (Int V)) is open Element of K10( the U1 of X)
V /\ (Int (Cl (Int V))) is Element of K10( the U1 of X)
(X,f) is Element of K10( the U1 of X)
Int f is open Element of K10( the U1 of X)
Cl (Int f) is closed Element of K10( the U1 of X)
Int (Cl (Int f)) is open Element of K10( the U1 of X)
f /\ (Int (Cl (Int f))) is Element of K10( the U1 of X)
Y is set
f is Element of K10( the U1 of X)
Int f is open Element of K10( the U1 of X)
Cl (Int f) is closed Element of K10( the U1 of X)
Int (Cl (Int f)) is open Element of K10( the U1 of X)
(X,f) is Element of K10( the U1 of X)
f /\ (Int (Cl (Int f))) is Element of K10( the U1 of X)

the U1 of X is set
K10( the U1 of X) is non empty set
(X) is Element of K10(K10( the U1 of X))
K10(K10( the U1 of X)) is non empty set
{ b1 where b1 is Element of K10( the U1 of X) : b1 is (X) } is set
(X) is Element of K10(K10( the U1 of X))
{ b1 where b1 is Element of K10( the U1 of X) : Int b1 = (X,b1) } is set
(X) /\ (X) is Element of K10(K10( the U1 of X))
the topology of X is non empty Element of K10(K10( the U1 of X))
Y is set
f is Element of K10( the U1 of X)
V is Element of K10( the U1 of X)
Int V is open Element of K10( the U1 of X)
(X,V) is Element of K10( the U1 of X)
Cl (Int V) is closed Element of K10( the U1 of X)
V /\ (Cl (Int V)) is Element of K10( the U1 of X)
(X,f) is Element of K10( the U1 of X)
Int f is open Element of K10( the U1 of X)
Cl (Int f) is closed Element of K10( the U1 of X)
f /\ (Cl (Int f)) is Element of K10( the U1 of X)
Y is set
f is Element of K10( the U1 of X)
Int f is open Element of K10( the U1 of X)
Cl (Int f) is closed Element of K10( the U1 of X)
(X,f) is Element of K10( the U1 of X)
f /\ (Cl (Int f)) is Element of K10( the U1 of X)

the U1 of X is set
K10( the U1 of X) is non empty set
(X) is Element of K10(K10( the U1 of X))
K10(K10( the U1 of X)) is non empty set
{ b1 where b1 is Element of K10( the U1 of X) : b1 is (X) } is set
(X) is Element of K10(K10( the U1 of X))
{ b1 where b1 is Element of K10( the U1 of X) : Int b1 = (X,b1) } is set
(X) /\ (X) is Element of K10(K10( the U1 of X))
the topology of X is non empty Element of K10(K10( the U1 of X))
Y is set
f is Element of K10( the U1 of X)
V is Element of K10( the U1 of X)
Int V is open Element of K10( the U1 of X)
(X,V) is Element of K10( the U1 of X)
Cl V is closed Element of K10( the U1 of X)
Int (Cl V) is open Element of K10( the U1 of X)
V /\ (Int (Cl V)) is Element of K10( the U1 of X)
(X,f) is Element of K10( the U1 of X)
Cl f is closed Element of K10( the U1 of X)
Int (Cl f) is open Element of K10( the U1 of X)
f /\ (Int (Cl f)) is Element of K10( the U1 of X)
Y is set
f is Element of K10( the U1 of X)
Int f is open Element of K10( the U1 of X)
Cl f is closed Element of K10( the U1 of X)
Int (Cl f) is open Element of K10( the U1 of X)
(X,f) is Element of K10( the U1 of X)
f /\ (Int (Cl f)) is Element of K10( the U1 of X)

the U1 of X is set
K10( the U1 of X) is non empty set
(X) is Element of K10(K10( the U1 of X))
K10(K10( the U1 of X)) is non empty set
{ b1 where b1 is Element of K10( the U1 of X) : b1 is (X) } is set
(X) is Element of K10(K10( the U1 of X))
{ b1 where b1 is Element of K10( the U1 of X) : Int b1 = (X,b1) } is set
(X) /\ (X) is Element of K10(K10( the U1 of X))
the topology of X is non empty Element of K10(K10( the U1 of X))
Y is set
f is Element of K10( the U1 of X)
V is Element of K10( the U1 of X)
Int V is open Element of K10( the U1 of X)
(X,V) is Element of K10( the U1 of X)
Cl V is closed Element of K10( the U1 of X)
Int (Cl V) is open Element of K10( the U1 of X)
Cl (Int (Cl V)) is closed Element of K10( the U1 of X)
V /\ (Cl (Int (Cl V))) is Element of K10( the U1 of X)
(X,f) is Element of K10( the U1 of X)
Cl f is closed Element of K10( the U1 of X)
Int (Cl f) is open Element of K10( the U1 of X)
Cl (Int (Cl f)) is closed Element of K10( the U1 of X)
f /\ (Cl (Int (Cl f))) is Element of K10( the U1 of X)
Y is set
f is Element of K10( the U1 of X)
Cl f is closed Element of K10( the U1 of X)
Int (Cl f) is open Element of K10( the U1 of X)
Cl (Int (Cl f)) is closed Element of K10( the U1 of X)
Int f is open Element of K10( the U1 of X)
(X,f) is Element of K10( the U1 of X)
f /\ (Cl (Int (Cl f))) is Element of K10( the U1 of X)

the U1 of X is set
K10( the U1 of X) is non empty set
(X) is Element of K10(K10( the U1 of X))
K10(K10( the U1 of X)) is non empty set
{ b1 where b1 is Element of K10( the U1 of X) : b1 is (X) } is set
(X) is Element of K10(K10( the U1 of X))
{ b1 where b1 is Element of K10( the U1 of X) : (X,b1) = (X,b1) } is set
(X) /\ (X) is Element of K10(K10( the U1 of X))
(X) is Element of K10(K10( the U1 of X))
{ b1 where b1 is Element of K10( the U1 of X) : b1 is (X) } is set
Y is set
f is Element of K10( the U1 of X)
V is Element of K10( the U1 of X)
(X,V) is Element of K10( the U1 of X)
Int V is open Element of K10( the U1 of X)
Cl (Int V) is closed Element of K10( the U1 of X)
Int (Cl (Int V)) is open Element of K10( the U1 of X)
V /\ (Int (Cl (Int V))) is Element of K10( the U1 of X)
(X,V) is Element of K10( the U1 of X)
Cl V is closed Element of K10( the U1 of X)
Int (Cl V) is open Element of K10( the U1 of X)
V /\ (Int (Cl V)) is Element of K10( the U1 of X)
(X,f) is Element of K10( the U1 of X)
Cl f is closed Element of K10( the U1 of X)
Int (Cl f) is open Element of K10( the U1 of X)
f /\ (Int (Cl f)) is Element of K10( the U1 of X)
Y is set
f is Element of K10( the U1 of X)
Int f is open Element of K10( the U1 of X)
Cl (Int f) is closed Element of K10( the U1 of X)
Cl f is closed Element of K10( the U1 of X)
Int (Cl (Int f)) is open Element of K10( the U1 of X)
Int (Cl f) is open Element of K10( the U1 of X)
(X,f) is Element of K10( the U1 of X)
f /\ (Int (Cl f)) is Element of K10( the U1 of X)
(X,f) is Element of K10( the U1 of X)
f /\ (Int (Cl (Int f))) is Element of K10( the U1 of X)

the U1 of X is set
K10( the U1 of X) is non empty set
(X) is Element of K10(K10( the U1 of X))
K10(K10( the U1 of X)) is non empty set
{ b1 where b1 is Element of K10( the U1 of X) : b1 is (X) } is set
(X) is Element of K10(K10( the U1 of X))
{ b1 where b1 is Element of K10( the U1 of X) : (X,b1) = (X,b1) } is set
(X) /\ (X) is Element of K10(K10( the U1 of X))
(X) is Element of K10(K10( the U1 of X))
{ b1 where b1 is Element of K10( the U1 of X) : b1 is (X) } is set
Y is set
f is Element of K10( the U1 of X)
V is Element of K10( the U1 of X)
(X,V) is Element of K10( the U1 of X)
Int V is open Element of K10( the U1 of X)
Cl (Int V) is closed Element of K10( the U1 of X)
Int (Cl (Int V)) is open Element of K10( the U1 of X)
V /\ (Int (Cl (Int V))) is Element of K10( the U1 of X)
(X,V) is Element of K10( the U1 of X)
V /\ (Cl (Int V)) is Element of K10( the U1 of X)
(X,f) is Element of K10( the U1 of X)
Int f is open Element of K10( the U1 of X)
Cl (Int f) is closed Element of K10( the U1 of X)
f /\ (Cl (Int f)) is Element of K10( the U1 of X)
Y is set
f is Element of K10( the U1 of X)
Int f is open Element of K10( the U1 of X)
Cl (Int f) is closed Element of K10( the U1 of X)
Int (Cl (Int f)) is open Element of K10( the U1 of X)
(X,f) is Element of K10( the U1 of X)
f /\ (Cl (Int f)) is Element of K10( the U1 of X)
(X,f) is Element of K10( the U1 of X)
f /\ (Int (Cl (Int f))) is Element of K10( the U1 of X)

the U1 of X is set
K10( the U1 of X) is non empty set
(X) is Element of K10(K10( the U1 of X))
K10(K10( the U1 of X)) is non empty set
{ b1 where b1 is Element of K10( the U1 of X) : b1 is (X) } is set
(X) is Element of K10(K10( the U1 of X))
{ b1 where b1 is Element of K10( the U1 of X) : (X,b1) = (X,b1) } is set
(X) /\ (X) is Element of K10(K10( the U1 of X))
(X) is Element of K10(K10( the U1 of X))
{ b1 where b1 is Element of K10( the U1 of X) : b1 is (X) } is set
Y is set
f is Element of K10( the U1 of X)
V is Element of K10( the U1 of X)
(X,V) is Element of K10( the U1 of X)
Int V is open Element of K10( the U1 of X)
Cl (Int V) is closed Element of K10( the U1 of X)
Int (Cl (Int V)) is open Element of K10( the U1 of X)
V /\ (Int (Cl (Int V))) is Element of K10( the U1 of X)
(X,V) is Element of K10( the U1 of X)
Cl V is closed Element of K10( the U1 of X)
Int (Cl V) is open Element of K10( the U1 of X)
Cl (Int (Cl V)) is closed Element of K10( the U1 of X)
V /\ (Cl (Int (Cl V))) is Element of K10( the U1 of X)
(X,f) is Element of K10( the U1 of X)
Cl f is closed Element of K10( the U1 of X)
Int (Cl f) is open Element of K10( the U1 of X)
Cl (Int (Cl f)) is closed Element of K10( the U1 of X)
f /\ (Cl (Int (Cl f))) is Element of K10( the U1 of X)
Y is set
f is Element of K10( the U1 of X)
Int f is open Element of K10( the U1 of X)
Cl (Int f) is closed Element of K10( the U1 of X)
Cl f is closed Element of K10( the U1 of X)
Int (Cl (Int f)) is open Element of K10( the U1 of X)
Int (Cl f) is open Element of K10( the U1 of X)
Cl (Int (Cl f)) is closed Element of K10( the U1 of X)
(X,f) is Element of K10( the U1 of X)
f /\ (Cl (Int (Cl f))) is Element of K10( the U1 of X)
(X,f) is Element of K10( the U1 of X)
f /\ (Int (Cl (Int f))) is Element of K10( the U1 of X)

the U1 of X is set
K10( the U1 of X) is non empty set
(X) is Element of K10(K10( the U1 of X))
K10(K10( the U1 of X)) is non empty set
{ b1 where b1 is Element of K10( the U1 of X) : b1 is (X) } is set
(X) is Element of K10(K10( the U1 of X))
{ b1 where b1 is Element of K10( the U1 of X) : (X,b1) = (X,b1) } is set
(X) /\ (X) is Element of K10(K10( the U1 of X))
(X) is Element of K10(K10( the U1 of X))
{ b1 where b1 is Element of K10( the U1 of X) : b1 is (X) } is set
Y is set
f is Element of K10( the U1 of X)
V is Element of K10( the U1 of X)
(X,V) is Element of K10( the U1 of X)
Cl V is closed Element of K10( the U1 of X)
Int (Cl V) is open Element of K10( the U1 of X)
V /\ (Int (Cl V)) is Element of K10( the U1 of X)
(X,V) is Element of K10( the U1 of X)
(X,V) is Element of K10( the U1 of X)
Int V is open Element of K10( the U1 of X)
Cl (Int V) is closed Element of K10( the U1 of X)
V /\ (Cl (Int V)) is Element of K10( the U1 of X)
(X,V) \/ (X,V) is Element of K10( the U1 of X)
(X,f) is Element of K10( the U1 of X)
(X,f) is Element of K10( the U1 of X)
Int f is open Element of K10( the U1 of X)
Cl (Int f) is closed Element of K10( the U1 of X)
f /\ (Cl (Int f)) is Element of K10( the U1 of X)
(X,f) is Element of K10( the U1 of X)
Cl f is closed Element of K10( the U1 of X)
Int (Cl f) is open Element of K10( the U1 of X)
f /\ (Int (Cl f)) is Element of K10( the U1 of X)
(X,f) \/ (X,f) is Element of K10( the U1 of X)
Y is set
f is Element of K10( the U1 of X)
Cl f is closed Element of K10( the U1 of X)
Int (Cl f) is open Element of K10( the U1 of X)
Int f is open Element of K10( the U1 of X)
Cl (Int f) is closed Element of K10( the U1 of X)
(Cl (Int f)) \/ (Int (Cl f)) is Element of K10( the U1 of X)
(X,f) is Element of K10( the U1 of X)
(X,f) is Element of K10( the U1 of X)
f /\ (Cl (Int f)) is Element of K10( the U1 of X)
(X,f) is Element of K10( the U1 of X)
f /\ (Int (Cl f)) is Element of K10( the U1 of X)
(X,f) \/ (X,f) is Element of K10( the U1 of X)

the U1 of X is set
K10( the U1 of X) is non empty set
(X) is Element of K10(K10( the U1 of X))
K10(K10( the U1 of X)) is non empty set
{ b1 where b1 is Element of K10( the U1 of X) : b1 is (X) } is set
(X) is Element of K10(K10( the U1 of X))
{ b1 where b1 is Element of K10( the U1 of X) : (X,b1) = (X,b1) } is set
(X) /\ (X) is Element of K10(K10( the U1 of X))
(X) is Element of K10(K10( the U1 of X))
{ b1 where b1 is Element of K10( the U1 of X) : b1 is (X) } is set
Y is set
f is Element of K10( the U1 of X)
V is Element of K10( the U1 of X)
(X,V) is Element of K10( the U1 of X)
Cl V is closed Element of K10( the U1 of X)
Int (Cl V) is open Element of K10( the U1 of X)
V /\ (Int (Cl V)) is Element of K10( the U1 of X)
(X,V) is Element of K10( the U1 of X)
Cl (Int (Cl V)) is closed Element of K10( the U1 of X)
V /\ (Cl (Int (Cl V))) is Element of K10( the U1 of X)
(X,f) is Element of K10( the U1 of X)
Cl f is closed Element of K10( the U1 of X)
Int (Cl f) is open Element of K10( the U1 of X)
Cl (Int (Cl f)) is closed Element of K10( the U1 of X)
f /\ (Cl (Int (Cl f))) is Element of K10( the U1 of X)
Y is set
f is Element of K10( the U1 of X)
Cl f is closed Element of K10( the U1 of X)
Int (Cl f) is open Element of K10( the U1 of X)
Cl (Int (Cl f)) is closed Element of K10( the U1 of X)
(X,f) is Element of K10( the U1 of X)
f /\ (Cl (Int (Cl f))) is Element of K10( the U1 of X)
(X,f) is Element of K10( the U1 of X)
f /\ (Int (Cl f)) is Element of K10( the U1 of X)

the U1 of X is set
K10( the U1 of X) is non empty set
(X) is Element of K10(K10( the U1 of X))
K10(K10( the U1 of X)) is non empty set
{ b1 where b1 is Element of K10( the U1 of X) : b1 is (X) } is set
(X) is Element of K10(K10( the U1 of X))
{ b1 where b1 is Element of K10( the U1 of X) : (X,b1) = (X,b1) } is set
(X) /\ (X) is Element of K10(K10( the U1 of X))
(X) is Element of K10(K10( the U1 of X))
{ b1 where b1 is Element of K10( the U1 of X) : b1 is (X) } is set
Y is set
f is Element of K10( the U1 of X)
V is Element of K10( the U1 of X)
(X,V) is Element of K10( the U1 of X)
Int V is open Element of K10( the U1 of X)
Cl (Int V) is closed Element of K10( the U1 of X)
Int (Cl (Int V)) is open Element of K10( the U1 of X)
V /\ (Int (Cl (Int V))) is Element of K10( the U1 of X)
(X,V) is Element of K10( the U1 of X)
Cl V is closed Element of K10( the U1 of X)
Int (Cl V) is open Element of K10( the U1 of X)
V /\ (Int (Cl V)) is Element of K10( the U1 of X)
(X,f) is Element of K10( the U1 of X)
Cl f is closed Element of K10( the U1 of X)
Int (Cl f) is open Element of K10( the U1 of X)
Cl (Int (Cl f)) is closed Element of K10( the U1 of X)
f /\ (Cl (Int (Cl f))) is Element of K10( the U1 of X)
(X,V) is Element of K10( the U1 of X)
V /\ (Cl (Int V)) is Element of K10( the U1 of X)
Y is set
f is Element of K10( the U1 of X)
Int f is open Element of K10( the U1 of X)
Cl (Int f) is closed Element of K10( the U1 of X)
Cl f is closed Element of K10( the U1 of X)
Int (Cl (Int f)) is open Element of K10( the U1 of X)
Int (Cl f) is open Element of K10( the U1 of X)
Cl (Int (Cl (Int f))) is closed Element of K10( the U1 of X)
Cl (Int (Cl f)) is closed Element of K10( the U1 of X)
(X,f) is Element of K10( the U1 of X)
f /\ (Cl (Int (Cl f))) is Element of K10( the U1 of X)
(X,f) is Element of K10( the U1 of X)
f /\ (Cl (Int f)) is Element of K10( the U1 of X)
(X,f) is Element of K10( the U1 of X)
f /\ (Int (Cl (Int f))) is Element of K10( the U1 of X)
(X,f) is Element of K10( the U1 of X)
f /\ (Int (Cl f)) is Element of K10( the U1 of X)

the U1 of X is set
K10( the U1 of X) is non empty set
(X) is Element of K10(K10( the U1 of X))
K10(K10( the U1 of X)) is non empty set
{ b1 where b1 is Element of K10( the U1 of X) : b1 is (X) } is set
(X) is Element of K10(K10( the U1 of X))
{ b1 where b1 is Element of K10( the U1 of X) : (X,b1) = (X,b1) } is set
(X) /\ (X) is Element of K10(K10( the U1 of X))
(X) is Element of K10(K10( the U1 of X))
{ b1 where b1 is Element of K10( the U1 of X) : b1 is (X) } is set
Y is set
f is Element of K10( the U1 of X)
V is Element of K10( the U1 of X)
(X,V) is Element of K10( the U1 of X)
(X,V) is Element of K10( the U1 of X)
Int V is open Element of K10( the U1 of X)
Cl (Int V) is closed Element of K10( the U1 of X)
V /\ (Cl (Int V)) is Element of K10( the U1 of X)
(X,V) is Element of K10( the U1 of X)
Cl V is closed Element of K10( the U1 of X)
Int (Cl V) is open Element of K10( the U1 of X)
V /\ (Int (Cl V)) is Element of K10( the U1 of X)
(X,V) \/ (X,V) is Element of K10( the U1 of X)
(X,V) is Element of K10( the U1 of X)
Cl (Int (Cl V)) is closed Element of K10( the U1 of X)
V /\ (Cl (Int (Cl V))) is Element of K10( the U1 of X)
(X,f) is Element of K10( the U1 of X)
Cl f is closed Element of K10( the U1 of X)
Int (Cl f) is open Element of K10( the U1 of X)
Cl (Int (Cl f)) is closed Element of K10( the U1 of X)
f /\ (Cl (Int (Cl f))) is Element of K10( the U1 of X)
Y is set
f is Element of K10( the U1 of X)
Int f is open Element of K10( the U1 of X)
Cl (Int f) is closed Element of K10( the U1 of X)
Cl f is closed Element of K10( the U1 of X)
Int (Cl (Int f)) is open Element of K10( the U1 of X)
Int (Cl f) is open Element of K10( the U1 of X)
Cl (Int (Cl (Int f))) is closed Element of K10( the U1 of X)
Cl (Int (Cl f)) is closed Element of K10( the U1 of X)
(Cl (Int f)) \/ (Int (Cl f)) is Element of K10( the U1 of X)
(X,f) is Element of K10( the U1 of X)
f /\ (Cl (Int (Cl f))) is Element of K10( the U1 of X)
(X,f) is Element of K10( the U1 of X)
(X,f) is Element of K10( the U1 of X)
f /\ (Cl (Int f)) is Element of K10( the U1 of X)
(X,f) is Element of K10( the U1 of X)
f /\ (Int (Cl f)) is Element of K10( the U1 of X)
(X,f) \/ (X,f) is Element of K10( the U1 of X)
X is non empty TopSpace-like TopStruct
the U1 of X is set
Y is non empty TopSpace-like TopStruct
the U1 of Y is set
K11( the U1 of X, the U1 of Y) is set
K10(K11( the U1 of X, the U1 of Y)) is non empty set
X is non empty TopSpace-like TopStruct
the U1 of X is set
Y is non empty TopSpace-like TopStruct
the U1 of Y is set
K11( the U1 of X, the U1 of Y) is set
K10(K11( the U1 of X, the U1 of Y)) is non empty set
f is V9() V18( the U1 of X, the U1 of Y) Element of K10(K11( the U1 of X, the U1 of Y))
K10( the U1 of Y) is non empty set
V is Element of K10( the U1 of Y)
f " V is Element of K10( the U1 of X)
K10( the U1 of X) is non empty set
(X) is Element of K10(K10( the U1 of X))
K10(K10( the U1 of X)) is non empty set
{ b1 where b1 is Element of K10( the U1 of X) : b1 is (X) } is set
(X) is Element of K10(K10( the U1 of X))
{ b1 where b1 is Element of K10( the U1 of X) : b1 is (X) } is set
(X) is Element of K10(K10( the U1 of X))
{ b1 where b1 is Element of K10( the U1 of X) : (X,b1) = (X,b1) } is set
(X) /\ (X) is Element of K10(K10( the U1 of X))
K10( the U1 of Y) is non empty set
V is Element of K10( the U1 of Y)
f " V is Element of K10( the U1 of X)
K10( the U1 of X) is non empty set
(X) is Element of K10(K10( the U1 of X))
K10(K10( the U1 of X)) is non empty set
{ b1 where b1 is Element of K10( the U1 of X) : (X,b1) = (X,b1) } is set
(X) is Element of K10(K10( the U1 of X))
{ b1 where b1 is Element of K10( the U1 of X) : b1 is (X) } is set
(X) is Element of K10(K10( the U1 of X))
{ b1 where b1 is Element of K10( the U1 of X) : b1 is (X) } is set
(X) /\ (X) is Element of K10(K10( the U1 of X))
K10( the U1 of Y) is non empty set
V is Element of K10( the U1 of Y)
f " V is Element of K10( the U1 of X)
K10( the U1 of X) is non empty set
(X) is Element of K10(K10( the U1 of X))
K10(K10( the U1 of X)) is non empty set
{ b1 where b1 is Element of K10( the U1 of X) : b1 is (X) } is set
(X) is Element of K10(K10( the U1 of X))
{ b1 where b1 is Element of K10( the U1 of X) : b1 is (X) } is set
(X) is Element of K10(K10( the U1 of X))
{ b1 where b1 is Element of K10( the U1 of X) : (X,b1) = (X,b1) } is set
(X) /\ (X) is Element of K10(K10( the U1 of X))
X is non empty TopSpace-like TopStruct
the U1 of X is set
Y is non empty TopSpace-like TopStruct
the U1 of Y is set
K11( the U1 of X, the U1 of Y) is set
K10(K11( the U1 of X, the U1 of Y)) is non empty set
f is V9() V18( the U1 of X, the U1 of Y) Element of K10(K11( the U1 of X, the U1 of Y))
K10( the U1 of Y) is non empty set
V is Element of K10( the U1 of Y)
f " V is Element of K10( the U1 of X)
K10( the U1 of X) is non empty set
(X) is Element of K10(K10( the U1 of X))
K10(K10( the U1 of X)) is non empty set
{ b1 where b1 is Element of K10( the U1 of X) : b1 is (X) } is set
(X) is Element of K10(K10( the U1 of X))
{ b1 where b1 is Element of K10( the U1 of X) : b1 is (X) } is set
(X) is Element of K10(K10( the U1 of X))
{ b1 where b1 is Element of K10( the U1 of X) : (X,b1) = (X,b1) } is set
(X) /\ (X) is Element of K10(K10( the U1 of X))
K10( the U1 of Y) is non empty set
V is Element of K10( the U1 of Y)
f " V is Element of K10( the U1 of X)
K10( the U1 of X) is non empty set
(X) is Element of K10(K10( the U1 of X))
K10(K10( the U1 of X)) is non empty set
{ b1 where b1 is Element of K10( the U1 of X) : (X,b1) = (X,b1) } is set
(X) is Element of K10(K10( the U1 of X))
{ b1 where b1 is Element of K10( the U1 of X) : b1 is (X) } is set
(X) is Element of K10(K10( the U1 of X))
{ b1 where b1 is Element of K10( the U1 of X) : b1 is (X) } is set
(X) /\ (X) is Element of K10(K10( the U1 of X))
K10( the U1 of Y) is non empty set
V is Element of K10( the U1 of Y)
f " V is Element of K10( the U1 of X)
K10( the U1 of X) is non empty set
(X) is Element of K10(K10( the U1 of X))
K10(K10( the U1 of X)) is non empty set
{ b1 where b1 is Element of K10( the U1 of X) : b1 is (X) } is set
(X) is Element of K10(K10( the U1 of X))
{ b1 where b1 is Element of K10( the U1 of X) : b1 is (X) } is set
(X) is Element of K10(K10( the U1 of X))
{ b1 where b1 is Element of K10( the U1 of X) : (X,b1) = (X,b1) } is set
(X) /\ (X) is Element of K10(K10( the U1 of X))
X is non empty TopSpace-like TopStruct
the U1 of X is set
Y is non empty TopSpace-like TopStruct
the U1 of Y is set
K11( the U1 of X, the U1 of Y) is set
K10(K11( the U1 of X, the U1 of Y)) is non empty set
f is V9() V18( the U1 of X, the U1 of Y) Element of K10(K11( the U1 of X, the U1 of Y))
K10( the U1 of Y) is non empty set
V is Element of K10( the U1 of Y)
f " V is Element of K10( the U1 of X)
K10( the U1 of X) is non empty set
(X) is Element of K10(K10( the U1 of X))
K10(K10( the U1 of X)) is non empty set
{ b1 where b1 is Element of K10( the U1 of X) : b1 is (X) } is set
(X) is Element of K10(K10( the U1 of X))
{ b1 where b1 is Element of K10( the U1 of X) : b1 is (X) } is set
(X) is Element of K10(K10( the U1 of X))
{ b1 where b1 is Element of K10( the U1 of X) : (X,b1) = (X,b1) } is set
(X) /\ (X) is Element of K10(K10( the U1 of X))
K10( the U1 of Y) is non empty set
V is Element of K10( the U1 of Y)
f " V is Element of K10( the U1 of X)
K10( the U1 of X) is non empty set
(X) is Element of K10(K10( the U1 of X))
K10(K10( the U1 of X)) is non empty set
{ b1 where b1 is Element of K10( the U1 of X) : (X,b1) = (X,b1) } is set
(X) is Element of K10(K10( the U1 of X))
{ b1 where b1 is Element of K10( the U1 of X) : b1 is (X) } is set
(X) is Element of K10(K10( the U1 of X))
{ b1 where b1 is Element of K10( the U1 of X) : b1 is (X) } is set
(X) /\ (X) is Element of K10(K10( the U1 of X))
K10( the U1 of Y) is non empty set
V is Element of K10( the U1 of Y)
f " V is Element of K10( the U1 of X)
K10( the U1 of X) is non empty set
(X) is Element of K10(K10( the U1 of X))
K10(K10( the U1 of X)) is non empty set
{ b1 where b1 is Element of K10( the U1 of X) : b1 is (X) } is set
(X) is Element of K10(K10( the U1 of X))
{ b1 where b1 is Element of K10( the U1 of X) : b1 is (X) } is set
(X) is Element of K10(K10( the U1 of X))
{ b1 where b1 is Element of K10( the U1 of X) : (X,b1) = (X,b1) } is set
(X) /\ (X) is Element of K10(K10( the U1 of X))
X is non empty TopSpace-like TopStruct
the U1 of X is set
Y is non empty TopSpace-like TopStruct
the U1 of Y is set
K11( the U1 of X, the U1 of Y) is set
K10(K11( the U1 of X, the U1 of Y)) is non empty set
f is V9() V18( the U1 of X, the U1 of Y) Element of K10(K11( the U1 of X, the U1 of Y))
K10( the U1 of Y) is non empty set
V is Element of K10( the U1 of Y)
f " V is Element of K10( the U1 of X)
K10( the U1 of X) is non empty set
(X) is Element of K10(K10( the U1 of X))
K10(K10( the U1 of X)) is non empty set
{ b1 where b1 is Element of K10( the U1 of X) : b1 is (X) } is set
(X) is Element of K10(K10( the U1 of X))
{ b1 where b1 is Element of K10( the U1 of X) : b1 is (X) } is set
K10( the U1 of Y) is non empty set
V is Element of K10( the U1 of Y)
f " V is Element of K10( the U1 of X)
K10( the U1 of X) is non empty set
(X) is Element of K10(K10( the U1 of X))
K10(K10( the U1 of X)) is non empty set
{ b1 where b1 is Element of K10( the U1 of X) : (X,b1) = (X,b1) } is set
(X) is Element of K10(K10( the U1 of X))
{ b1 where b1 is Element of K10( the U1 of X) : b1 is (X) } is set
(X) is Element of K10(K10( the U1 of X))
{ b1 where b1 is Element of K10( the U1 of X) : b1 is (X) } is set
(X) /\ (X) is Element of K10(K10( the U1 of X))
K10( the U1 of Y) is non empty set
V is Element of K10( the U1 of Y)
f " V is Element of K10( the U1 of X)
K10( the U1 of X) is non empty set
(X) is Element of K10(K10( the U1 of X))
K10(K10( the U1 of X)) is non empty set
{ b1 where b1 is Element of K10( the U1 of X) : b1 is (X) } is set
(X) is Element of K10(K10( the U1 of X))
{ b1 where b1 is Element of K10( the U1 of X) : b1 is (X) } is set
X is non empty TopSpace-like TopStruct
the U1 of X is set
Y is non empty TopSpace-like TopStruct
the U1 of Y is set
K11( the U1 of X, the U1 of Y) is set
K10(K11( the U1 of X, the U1 of Y)) is non empty set
f is V9() V18( the U1 of X, the U1 of Y) Element of K10(K11( the U1 of X, the U1 of Y))
K10( the U1 of Y) is non empty set
V is Element of K10( the U1 of Y)
f " V is Element of K10( the U1 of X)
K10( the U1 of X) is non empty set
(X) is Element of K10(K10( the U1 of X))
K10(K10( the U1 of X)) is non empty set
{ b1 where b1 is Element of K10( the U1 of X) : b1 is (X) } is set
(X) is Element of K10(K10( the U1 of X))
{ b1 where b1 is Element of K10( the U1 of X) : b1 is (X) } is set
K10( the U1 of Y) is non empty set
V is Element of K10( the U1 of Y)
f " V is Element of K10( the U1 of X)
K10( the U1 of X) is non empty set
(X) is Element of K10(K10( the U1 of X))
K10(K10( the U1 of X)) is non empty set
{ b1 where b1 is Element of K10( the U1 of X) : (X,b1) = (X,b1) } is set
(X) is Element of K10(K10( the U1 of X))
{ b1 where b1 is Element of K10( the U1 of X) : b1 is (X) } is set
(X) is Element of K10(K10( the U1 of X))
{ b1 where b1 is Element of K10( the U1 of X) : b1 is (X) } is set
(X) /\ (X) is Element of K10(K10( the U1 of X))
K10( the U1 of Y) is non empty set
V is Element of K10( the U1 of Y)
f " V is Element of K10( the U1 of X)
K10( the U1 of X) is non empty set
(X) is Element of K10(K10( the U1 of X))
K10(K10( the U1 of X)) is non empty set
{ b1 where b1 is Element of K10( the U1 of X) : b1 is (X) } is set
(X) is Element of K10(K10( the U1 of X))
{ b1 where b1 is Element of K10( the U1 of X) : b1 is (X) } is set
X is non empty TopSpace-like TopStruct
the U1 of X is set
Y is non empty TopSpace-like TopStruct
the U1 of Y is set
K11( the U1 of X, the U1 of Y) is set
K10(K11( the U1 of X, the U1 of Y)) is non empty set
f is V9() V18( the U1 of X, the U1 of Y) Element of K10(K11( the U1 of X, the U1 of Y))
K10( the U1 of Y) is non empty set
V is Element of K10( the U1 of Y)
f " V is Element of K10( the U1 of X)
K10( the U1 of X) is non empty set
(X) is Element of K10(K10( the U1 of X))
K10(K10( the U1 of X)) is non empty set
{ b1 where b1 is Element of K10( the U1 of X) : b1 is (X) } is set
(X) is Element of K10(K10( the U1 of X))
{ b1 where b1 is Element of K10( the U1 of X) : b1 is (X) } is set
K10( the U1 of Y) is non empty set
V is Element of K10( the U1 of Y)
f " V is Element of K10( the U1 of X)
K10( the U1 of X) is non empty set
(X) is Element of K10(K10( the U1 of X))
K10(K10( the U1 of X)) is non empty set
{ b1 where b1 is Element of K10( the U1 of X) : (X,b1) = (X,b1) } is set
(X) is Element of K10(K10( the U1 of X))
{ b1 where b1 is Element of K10( the U1 of X) : b1 is (X) } is set
(X) is Element of K10(K10( the U1 of X))
{ b1 where b1 is Element of K10( the U1 of X) : b1 is (X) } is set
(X) /\ (X) is Element of K10(K10( the U1 of X))
K10( the U1 of Y) is non empty set
V is Element of K10( the U1 of Y)
f " V is Element of K10( the U1 of X)
K10( the U1 of X) is non empty set
(X) is Element of K10(K10( the U1 of X))
K10(K10( the U1 of X)) is non empty set
{ b1 where b1 is Element of K10( the U1 of X) : b1 is (X) } is set
(X) is Element of K10(K10( the U1 of X))
{ b1 where b1 is Element of K10( the U1 of X) : b1 is (X) } is set
X is non empty TopSpace-like TopStruct
the U1 of X is set
Y is non empty TopSpace-like TopStruct
the U1 of Y is set
K11( the U1 of X, the U1 of Y) is set
K10(K11( the U1 of X, the U1 of Y)) is non empty set
f is V9() V18( the U1 of X, the U1 of Y) Element of K10(K11( the U1 of X, the U1 of Y))
K10( the U1 of Y) is non empty set
V is Element of K10( the U1 of Y)
f " V is Element of K10( the U1 of X)
K10( the U1 of X) is non empty set
(X) is Element of K10(K10( the U1 of X))
K10(K10( the U1 of X)) is non empty set
{ b1 where b1 is Element of K10( the U1 of X) : b1 is (X) } is set
(X) is Element of K10(K10( the U1 of X))
{ b1 where b1 is Element of K10( the U1 of X) : b1 is (X) } is set
K10( the U1 of Y) is non empty set
V is Element of K10( the U1 of Y)
f " V is Element of K10( the U1 of X)
K10( the U1 of X) is non empty set
(X) is Element of K10(K10( the U1 of X))
K10(K10( the U1 of X)) is non empty set
{ b1 where b1 is Element of K10( the U1 of X) : (X,b1) = (X,b1) } is set
(X) is Element of K10(K10( the U1 of X))
{ b1 where b1 is Element of K10( the U1 of X) : b1 is (X) } is set
(X) is Element of K10(K10( the U1 of X))
{ b1 where b1 is Element of K10( the U1 of X) : b1 is (X) } is set
(X) /\ (X) is Element of K10(K10( the U1 of X))
K10( the U1 of Y) is non empty set
V is Element of K10( the U1 of Y)
f " V is Element of K10( the U1 of X)
K10( the U1 of X) is non empty set
(X) is Element of K10(K10( the U1 of X))
K10(K10( the U1 of X)) is non empty set
{ b1 where b1 is Element of K10( the U1 of X) : b1 is (X) } is set
(X) is Element of K10(K10( the U1 of X))
{ b1 where b1 is Element of K10( the U1 of X) : b1 is (X) } is set
X is non empty TopSpace-like TopStruct
the U1 of X is set
Y is non empty TopSpace-like TopStruct
the U1 of Y is set
K11( the U1 of X, the U1 of Y) is set
K10(K11( the U1 of X, the U1 of Y)) is non empty set
f is V9() V18( the U1 of X, the U1 of Y) Element of K10(K11( the U1 of X, the U1 of Y))
[#] Y is open closed dense non boundary Element of K10( the U1 of Y)
K10( the U1 of Y) is non empty set
V is Element of K10( the U1 of Y)
f " V is Element of K10( the U1 of X)
K10( the U1 of X) is non empty set
(X) is Element of K10(K10( the U1 of X))
K10(K10( the U1 of X)) is non empty set
{ b1 where b1 is Element of K10( the U1 of X) : b1 is (X) } is set
the topology of X is non empty Element of K10(K10( the U1 of X))
(X) is Element of K10(K10( the U1 of X))
{ b1 where b1 is Element of K10( the U1 of X) : Int b1 = (X,b1) } is set
(X) /\ (X) is Element of K10(K10( the U1 of X))
V is Element of K10( the U1 of Y)
f " V is Element of K10( the U1 of X)
K10( the U1 of X) is non empty set
(X) is Element of K10(K10( the U1 of X))
K10(K10( the U1 of X)) is non empty set
{ b1 where b1 is Element of K10( the U1 of X) : Int b1 = (X,b1) } is set
the topology of X is non empty Element of K10(K10( the U1 of X))
(X) is Element of K10(K10( the U1 of X))
{ b1 where b1 is Element of K10( the U1 of X) : b1 is (X) } is set
(X) /\ (X) is Element of K10(K10( the U1 of X))
V is Element of K10( the U1 of Y)
f " V is Element of K10( the U1 of X)
K10( the U1 of X) is non empty set
(X) is Element of K10(K10( the U1 of X))
K10(K10( the U1 of X)) is non empty set
{ b1 where b1 is Element of K10( the U1 of X) : b1 is (X) } is set
(X) is Element of K10(K10( the U1 of X))
{ b1 where b1 is Element of K10( the U1 of X) : Int b1 = (X,b1) } is set
(X) /\ (X) is Element of K10(K10( the U1 of X))
the topology of X is non empty Element of K10(K10( the U1 of X))
X is non empty TopSpace-like TopStruct
the U1 of X is set
Y is non empty TopSpace-like TopStruct
the U1 of Y is set
K11( the U1 of X, the U1 of Y) is set
K10(K11( the U1 of X, the U1 of Y)) is non empty set
f is V9() V18( the U1 of X, the U1 of Y) Element of K10(K11( the U1 of X, the U1 of Y))
[#] Y is open closed dense non boundary Element of K10( the U1 of Y)
K10( the U1 of Y) is non empty set
V is Element of K10( the U1 of Y)
f " V is Element of K10( the U1 of X)
K10( the U1 of X) is non empty set
(X) is Element of K10(K10( the U1 of X))
K10(K10( the U1 of X)) is non empty set
{ b1 where b1 is Element of K10( the U1 of X) : b1 is (X) } is set
the topology of X is non empty Element of K10(K10( the U1 of X))
(X) is Element of K10(K10( the U1 of X))
{ b1 where b1 is Element of K10( the U1 of X) : Int b1 = (X,b1) } is set
(X) /\ (X) is Element of K10(K10( the U1 of X))
V is Element of K10( the U1 of Y)
f " V is Element of K10( the U1 of X)
K10( the U1 of X) is non empty set
(X) is Element of K10(K10( the U1 of X))
K10(K10( the U1 of X)) is non empty set
{ b1 where b1 is Element of K10( the U1 of X) : Int b1 = (X,b1) } is set
the topology of X is non empty Element of K10(K10( the U1 of X))
(X) is Element of K10(K10( the U1 of X))
{ b1 where b1 is Element of K10( the U1 of X) : b1 is (X) } is set
(X) /\ (X) is Element of K10(K10( the U1 of X))
V is Element of K10( the U1 of Y)
f " V is Element of K10( the U1 of X)
K10( the U1 of X) is non empty set
(X) is Element of K10(K10( the U1 of X))
K10(K10( the U1 of X)) is non empty set
{ b1 where b1 is Element of K10( the U1 of X) : b1 is (X) } is set
(X) is Element of K10(K10( the U1 of X))
{ b1 where b1 is Element of K10( the U1 of X) : Int b1 = (X,b1) } is set
(X) /\ (X) is Element of K10(K10( the U1 of X))
the topology of X is non empty Element of K10(K10( the U1 of X))
X is non empty TopSpace-like TopStruct
the U1 of X is set
Y is non empty TopSpace-like TopStruct
the U1 of Y is set
K11( the U1 of X, the U1 of Y) is set
K10(K11( the U1 of X, the U1 of Y)) is non empty set
f is V9() V18( the U1 of X, the U1 of Y) Element of K10(K11( the U1 of X, the U1 of Y))
[#] Y is open closed dense non boundary Element of K10( the U1 of Y)
K10( the U1 of Y) is non empty set
V is Element of K10( the U1 of Y)
f " V is Element of K10( the U1 of X)
K10( the U1 of X) is non empty set
(X) is Element of K10(K10( the U1 of X))
K10(K10( the U1 of X)) is non empty set
{ b1 where b1 is Element of K10( the U1 of X) : b1 is (X) } is set
the topology of X is non empty Element of K10(K10( the U1 of X))
(X) is Element of K10(K10( the U1 of X))
{ b1 where b1 is Element of K10( the U1 of X) : Int b1 = (X,b1) } is set
(X) /\ (X) is Element of K10(K10( the U1 of X))
V is Element of K10( the U1 of Y)
f " V is Element of K10( the U1 of X)
K10( the U1 of X) is non empty set
(X) is Element of K10(K10( the U1 of X))
K10(K10( the U1 of X)) is non empty set
{ b1 where b1 is Element of K10( the U1 of X) : Int b1 = (X,b1) } is set
the topology of X is non empty Element of K10(K10( the U1 of X))
(X) is Element of K10(K10( the U1 of X))
{ b1 where b1 is Element of K10( the U1 of X) : b1 is (X) } is set
(X) /\ (X) is Element of K10(K10( the U1 of X))
V is Element of K10( the U1 of Y)
f " V is Element of K10( the U1 of X)
K10( the U1 of X) is non empty set
(X) is Element of K10(K10( the U1 of X))
K10(K10( the U1 of X)) is non empty set
{ b1 where b1 is Element of K10( the U1 of X) : b1 is (X) } is set
(X) is Element of K10(K10( the U1 of X))
{ b1 where b1 is Element of K10( the U1 of X) : Int b1 = (X,b1) } is set
(X) /\ (X) is Element of K10(K10( the U1 of X))
the topology of X is non empty Element of K10(K10( the U1 of X))
X is non empty TopSpace-like TopStruct
the U1 of X is set
Y is non empty TopSpace-like TopStruct
the U1 of Y is set
K11( the U1 of X, the U1 of Y) is set
K10(K11( the U1 of X, the U1 of Y)) is non empty set
f is V9() V18( the U1 of X, the U1 of Y) Element of K10(K11( the U1 of X, the U1 of Y))
[#] Y is open closed dense non boundary Element of K10( the U1 of Y)
K10( the U1 of Y) is non empty set
V is Element of K10( the U1 of Y)
f " V is Element of K10( the U1 of X)
K10( the U1 of X) is non empty set
(X) is Element of K10(K10( the U1 of X))
K10(K10( the U1 of X)) is non empty set
{ b1 where b1 is Element of K10( the U1 of X) : b1 is (X) } is set
the topology of X is non empty Element of K10(K10( the U1 of X))
(X) is Element of K10(K10( the U1 of X))
{ b1 where b1 is Element of K10( the U1 of X) : Int b1 = (X,b1) } is set
(X) /\ (X) is Element of K10(K10( the U1 of X))
V is Element of K10( the U1 of Y)
f " V is Element of K10( the U1 of X)
K10( the U1 of X) is non empty set
(X) is Element of K10(K10( the U1 of X))
K10(K10( the U1 of X)) is non empty set
{ b1 where b1 is Element of K10( the U1 of X) : Int b1 = (X,b1) } is set
the topology of X is non empty Element of K10(K10( the U1 of X))
(X) is Element of K10(K10( the U1 of X))
{ b1 where b1 is Element of K10( the U1 of X) : b1 is (X) } is set
(X) /\ (X) is Element of K10(K10( the U1 of X))
V is Element of K10( the U1 of Y)
f " V is Element of K10( the U1 of X)
K10( the U1 of X) is non empty set
(X) is Element of K10(K10( the U1 of X))
K10(K10( the U1 of X)) is non empty set
{ b1 where b1 is Element of K10( the U1 of X) : b1 is (X) } is set
(X) is Element of K10(K10( the U1 of X))
{ b1 where b1 is Element of K10( the U1 of X) : Int b1 = (X,b1) } is set
(X) /\ (X) is Element of K10(K10( the U1 of X))
the topology of X is non empty Element of K10(K10( the U1 of X))