:: 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)
X is TopSpace-like TopStruct
the U1 of X is set
K10( the U1 of X) is non empty set
{ b₁ where b₁ is Element of K10( the U1 of X) : b₁ is (X) } is set
K10(K10( the U1 of X)) is non empty set
{ b₁ where b₁ is Element of K10( the U1 of X) : S₁[b₁] } is set
{ b₁ where b₁ is Element of K10( the U1 of X) : b₁ is (X) } is set
{ b₁ where b₁ is Element of K10( the U1 of X) : S₁[b₁] } is set
{ b₁ where b₁ is Element of K10( the U1 of X) : b₁ is (X) } is set
{ b₁ where b₁ is Element of K10( the U1 of X) : S₁[b₁] } is set
{ b₁ where b₁ is Element of K10( the U1 of X) : b₁ is (X) } is set
{ b₁ where b₁ is Element of K10( the U1 of X) : S₁[b₁] } is set
{ b₁ where b₁ is Element of K10( the U1 of X) : b₁ is (X) } is set
{ b₁ where b₁ is Element of K10( the U1 of X) : S₁[b₁] } is set
{ b₁ where b₁ is Element of K10( the U1 of X) : Int b₁ = (X,b₁) } is set
{ b₁ where b₁ is Element of K10( the U1 of X) : S₁[b₁] } is set
{ b₁ where b₁ is Element of K10( the U1 of X) : Int b₁ = (X,b₁) } is set
{ b₁ where b₁ is Element of K10( the U1 of X) : S₁[b₁] } is set
{ b₁ where b₁ is Element of K10( the U1 of X) : Int b₁ = (X,b₁) } is set
{ b₁ where b₁ is Element of K10( the U1 of X) : S₁[b₁] } is set
{ b₁ where b₁ is Element of K10( the U1 of X) : Int b₁ = (X,b₁) } is set
{ b₁ where b₁ is Element of K10( the U1 of X) : S₁[b₁] } is set
{ b₁ where b₁ is Element of K10( the U1 of X) : (X,b₁) = (X,b₁) } is set
{ b₁ where b₁ is Element of K10( the U1 of X) : S₁[b₁] } is set
{ b₁ where b₁ is Element of K10( the U1 of X) : (X,b₁) = (X,b₁) } is set
{ b₁ where b₁ is Element of K10( the U1 of X) : S₁[b₁] } is set
{ b₁ where b₁ is Element of K10( the U1 of X) : (X,b₁) = (X,b₁) } is set
{ b₁ where b₁ is Element of K10( the U1 of X) : S₁[b₁] } is set
{ b₁ where b₁ is Element of K10( the U1 of X) : (X,b₁) = (X,b₁) } is set
{ b₁ where b₁ is Element of K10( the U1 of X) : S₁[b₁] } is set
{ b₁ where b₁ is Element of K10( the U1 of X) : (X,b₁) = (X,b₁) } is set
{ b₁ where b₁ is Element of K10( the U1 of X) : S₁[b₁] } is set
{ b₁ where b₁ is Element of K10( the U1 of X) : (X,b₁) = (X,b₁) } is set
{ b₁ where b₁ is Element of K10( the U1 of X) : S₁[b₁] } is set
X is TopSpace-like 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 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)
X is TopSpace-like 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 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 is TopSpace-like 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 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 is TopSpace-like 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)
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 is TopSpace-like 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)
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)
X is TopSpace-like 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)
(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)
X is TopSpace-like TopStruct
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
{ b₁ where b₁ is Element of K10( the U1 of X) : b₁ is (X) } is set
(X) is Element of K10(K10( the U1 of X))
{ b₁ where b₁ is Element of K10( the U1 of X) : Int b₁ = (X,b₁) } 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)
X is TopSpace-like TopStruct
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
{ b₁ where b₁ is Element of K10( the U1 of X) : b₁ is (X) } is set
(X) is Element of K10(K10( the U1 of X))
{ b₁ where b₁ is Element of K10( the U1 of X) : Int b₁ = (X,b₁) } 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)
X is TopSpace-like TopStruct
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
{ b₁ where b₁ is Element of K10( the U1 of X) : b₁ is (X) } is set
(X) is Element of K10(K10( the U1 of X))
{ b₁ where b₁ is Element of K10( the U1 of X) : Int b₁ = (X,b₁) } 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)
X is TopSpace-like TopStruct
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
{ b₁ where b₁ is Element of K10( the U1 of X) : b₁ is (X) } is set
(X) is Element of K10(K10( the U1 of X))
{ b₁ where b₁ is Element of K10( the U1 of X) : Int b₁ = (X,b₁) } 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)
X is TopSpace-like TopStruct
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
{ b₁ where b₁ is Element of K10( the U1 of X) : b₁ is (X) } is set
(X) is Element of K10(K10( the U1 of X))
{ b₁ where b₁ is Element of K10( the U1 of X) : (X,b₁) = (X,b₁) } is set
(X) /\ (X) is Element of K10(K10( the U1 of X))
(X) is Element of K10(K10( the U1 of X))
{ b₁ where b₁ is Element of K10( the U1 of X) : b₁ 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)
X is TopSpace-like TopStruct
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
{ b₁ where b₁ is Element of K10( the U1 of X) : b₁ is (X) } is set
(X) is Element of K10(K10( the U1 of X))
{ b₁ where b₁ is Element of K10( the U1 of X) : (X,b₁) = (X,b₁) } is set
(X) /\ (X) is Element of K10(K10( the U1 of X))
(X) is Element of K10(K10( the U1 of X))
{ b₁ where b₁ is Element of K10( the U1 of X) : b₁ 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)
X is TopSpace-like TopStruct
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
{ b₁ where b₁ is Element of K10( the U1 of X) : b₁ is (X) } is set
(X) is Element of K10(K10( the U1 of X))
{ b₁ where b₁ is Element of K10( the U1 of X) : (X,b₁) = (X,b₁) } is set
(X) /\ (X) is Element of K10(K10( the U1 of X))
(X) is Element of K10(K10( the U1 of X))
{ b₁ where b₁ is Element of K10( the U1 of X) : b₁ 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)
X is TopSpace-like TopStruct
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
{ b₁ where b₁ is Element of K10( the U1 of X) : b₁ is (X) } is set
(X) is Element of K10(K10( the U1 of X))
{ b₁ where b₁ is Element of K10( the U1 of X) : (X,b₁) = (X,b₁) } is set
(X) /\ (X) is Element of K10(K10( the U1 of X))
(X) is Element of K10(K10( the U1 of X))
{ b₁ where b₁ is Element of K10( the U1 of X) : b₁ 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)
X is TopSpace-like TopStruct
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
{ b₁ where b₁ is Element of K10( the U1 of X) : b₁ is (X) } is set
(X) is Element of K10(K10( the U1 of X))
{ b₁ where b₁ is Element of K10( the U1 of X) : (X,b₁) = (X,b₁) } is set
(X) /\ (X) is Element of K10(K10( the U1 of X))
(X) is Element of K10(K10( the U1 of X))
{ b₁ where b₁ is Element of K10( the U1 of X) : b₁ 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)
X is TopSpace-like TopStruct
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
{ b₁ where b₁ is Element of K10( the U1 of X) : b₁ is (X) } is set
(X) is Element of K10(K10( the U1 of X))
{ b₁ where b₁ is Element of K10( the U1 of X) : (X,b₁) = (X,b₁) } is set
(X) /\ (X) is Element of K10(K10( the U1 of X))
(X) is Element of K10(K10( the U1 of X))
{ b₁ where b₁ is Element of K10( the U1 of X) : b₁ 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)
X is TopSpace-like TopStruct
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
{ b₁ where b₁ is Element of K10( the U1 of X) : b₁ is (X) } is set
(X) is Element of K10(K10( the U1 of X))
{ b₁ where b₁ is Element of K10( the U1 of X) : (X,b₁) = (X,b₁) } is set
(X) /\ (X) is Element of K10(K10( the U1 of X))
(X) is Element of K10(K10( the U1 of X))
{ b₁ where b₁ is Element of K10( the U1 of X) : b₁ 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
{ b₁ where b₁ is Element of K10( the U1 of X) : b₁ is (X) } is set
(X) is Element of K10(K10( the U1 of X))
{ b₁ where b₁ is Element of K10( the U1 of X) : b₁ is (X) } is set
(X) is Element of K10(K10( the U1 of X))
{ b₁ where b₁ is Element of K10( the U1 of X) : (X,b₁) = (X,b₁) } 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
{ b₁ where b₁ is Element of K10( the U1 of X) : (X,b₁) = (X,b₁) } is set
(X) is Element of K10(K10( the U1 of X))
{ b₁ where b₁ is Element of K10( the U1 of X) : b₁ is (X) } is set
(X) is Element of K10(K10( the U1 of X))
{ b₁ where b₁ is Element of K10( the U1 of X) : b₁ 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
{ b₁ where b₁ is Element of K10( the U1 of X) : b₁ is (X) } is set
(X) is Element of K10(K10( the U1 of X))
{ b₁ where b₁ is Element of K10( the U1 of X) : b₁ is (X) } is set
(X) is Element of K10(K10( the U1 of X))
{ b₁ where b₁ is Element of K10( the U1 of X) : (X,b₁) = (X,b₁) } 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
{ b₁ where b₁ is Element of K10( the U1 of X) : b₁ is (X) } is set
(X) is Element of K10(K10( the U1 of X))
{ b₁ where b₁ is Element of K10( the U1 of X) : b₁ is (X) } is set
(X) is Element of K10(K10( the U1 of X))
{ b₁ where b₁ is Element of K10( the U1 of X) : (X,b₁) = (X,b₁) } 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
{ b₁ where b₁ is Element of K10( the U1 of X) : (X,b₁) = (X,b₁) } is set
(X) is Element of K10(K10( the U1 of X))
{ b₁ where b₁ is Element of K10( the U1 of X) : b₁ is (X) } is set
(X) is Element of K10(K10( the U1 of X))
{ b₁ where b₁ is Element of K10( the U1 of X) : b₁ 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
{ b₁ where b₁ is Element of K10( the U1 of X) : b₁ is (X) } is set
(X) is Element of K10(K10( the U1 of X))
{ b₁ where b₁ is Element of K10( the U1 of X) : b₁ is (X) } is set
(X) is Element of K10(K10( the U1 of X))
{ b₁ where b₁ is Element of K10( the U1 of X) : (X,b₁) = (X,b₁) } 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
{ b₁ where b₁ is Element of K10( the U1 of X) : b₁ is (X) } is set
(X) is Element of K10(K10( the U1 of X))
{ b₁ where b₁ is Element of K10( the U1 of X) : b₁ is (X) } is set
(X) is Element of K10(K10( the U1 of X))
{ b₁ where b₁ is Element of K10( the U1 of X) : (X,b₁) = (X,b₁) } 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
{ b₁ where b₁ is Element of K10( the U1 of X) : (X,b₁) = (X,b₁) } is set
(X) is Element of K10(K10( the U1 of X))
{ b₁ where b₁ is Element of K10( the U1 of X) : b₁ is (X) } is set
(X) is Element of K10(K10( the U1 of X))
{ b₁ where b₁ is Element of K10( the U1 of X) : b₁ 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
{ b₁ where b₁ is Element of K10( the U1 of X) : b₁ is (X) } is set
(X) is Element of K10(K10( the U1 of X))
{ b₁ where b₁ is Element of K10( the U1 of X) : b₁ is (X) } is set
(X) is Element of K10(K10( the U1 of X))
{ b₁ where b₁ is Element of K10( the U1 of X) : (X,b₁) = (X,b₁) } 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
{ b₁ where b₁ is Element of K10( the U1 of X) : b₁ is (X) } is set
(X) is Element of K10(K10( the U1 of X))
{ b₁ where b₁ is Element of K10( the U1 of X) : b₁ 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
{ b₁ where b₁ is Element of K10( the U1 of X) : (X,b₁) = (X,b₁) } is set
(X) is Element of K10(K10( the U1 of X))
{ b₁ where b₁ is Element of K10( the U1 of X) : b₁ is (X) } is set
(X) is Element of K10(K10( the U1 of X))
{ b₁ where b₁ is Element of K10( the U1 of X) : b₁ 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
{ b₁ where b₁ is Element of K10( the U1 of X) : b₁ is (X) } is set
(X) is Element of K10(K10( the U1 of X))
{ b₁ where b₁ is Element of K10( the U1 of X) : b₁ 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
{ b₁ where b₁ is Element of K10( the U1 of X) : b₁ is (X) } is set
(X) is Element of K10(K10( the U1 of X))
{ b₁ where b₁ is Element of K10( the U1 of X) : b₁ 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
{ b₁ where b₁ is Element of K10( the U1 of X) : (X,b₁) = (X,b₁) } is set
(X) is Element of K10(K10( the U1 of X))
{ b₁ where b₁ is Element of K10( the U1 of X) : b₁ is (X) } is set
(X) is Element of K10(K10( the U1 of X))
{ b₁ where b₁ is Element of K10( the U1 of X) : b₁ 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
{ b₁ where b₁ is Element of K10( the U1 of X) : b₁ is (X) } is set
(X) is Element of K10(K10( the U1 of X))
{ b₁ where b₁ is Element of K10( the U1 of X) : b₁ 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
{ b₁ where b₁ is Element of K10( the U1 of X) : b₁ is (X) } is set
(X) is Element of K10(K10( the U1 of X))
{ b₁ where b₁ is Element of K10( the U1 of X) : b₁ 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
{ b₁ where b₁ is Element of K10( the U1 of X) : (X,b₁) = (X,b₁) } is set
(X) is Element of K10(K10( the U1 of X))
{ b₁ where b₁ is Element of K10( the U1 of X) : b₁ is (X) } is set
(X) is Element of K10(K10( the U1 of X))
{ b₁ where b₁ is Element of K10( the U1 of X) : b₁ 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
{ b₁ where b₁ is Element of K10( the U1 of X) : b₁ is (X) } is set
(X) is Element of K10(K10( the U1 of X))
{ b₁ where b₁ is Element of K10( the U1 of X) : b₁ 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
{ b₁ where b₁ is Element of K10( the U1 of X) : b₁ is (X) } is set
(X) is Element of K10(K10( the U1 of X))
{ b₁ where b₁ is Element of K10( the U1 of X) : b₁ 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
{ b₁ where b₁ is Element of K10( the U1 of X) : (X,b₁) = (X,b₁) } is set
(X) is Element of K10(K10( the U1 of X))
{ b₁ where b₁ is Element of K10( the U1 of X) : b₁ is (X) } is set
(X) is Element of K10(K10( the U1 of X))
{ b₁ where b₁ is Element of K10( the U1 of X) : b₁ 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
{ b₁ where b₁ is Element of K10( the U1 of X) : b₁ is (X) } is set
(X) is Element of K10(K10( the U1 of X))
{ b₁ where b₁ is Element of K10( the U1 of X) : b₁ 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
{ b₁ where b₁ is Element of K10( the U1 of X) : b₁ 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))
{ b₁ where b₁ is Element of K10( the U1 of X) : Int b₁ = (X,b₁) } 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
{ b₁ where b₁ is Element of K10( the U1 of X) : Int b₁ = (X,b₁) } 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))
{ b₁ where b₁ is Element of K10( the U1 of X) : b₁ 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
{ b₁ where b₁ is Element of K10( the U1 of X) : b₁ is (X) } is set
(X) is Element of K10(K10( the U1 of X))
{ b₁ where b₁ is Element of K10( the U1 of X) : Int b₁ = (X,b₁) } 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
{ b₁ where b₁ is Element of K10( the U1 of X) : b₁ 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))
{ b₁ where b₁ is Element of K10( the U1 of X) : Int b₁ = (X,b₁) } 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
{ b₁ where b₁ is Element of K10( the U1 of X) : Int b₁ = (X,b₁) } 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))
{ b₁ where b₁ is Element of K10( the U1 of X) : b₁ 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
{ b₁ where b₁ is Element of K10( the U1 of X) : b₁ is (X) } is set
(X) is Element of K10(K10( the U1 of X))
{ b₁ where b₁ is Element of K10( the U1 of X) : Int b₁ = (X,b₁) } 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
{ b₁ where b₁ is Element of K10( the U1 of X) : b₁ 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))
{ b₁ where b₁ is Element of K10( the U1 of X) : Int b₁ = (X,b₁) } 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
{ b₁ where b₁ is Element of K10( the U1 of X) : Int b₁ = (X,b₁) } 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))
{ b₁ where b₁ is Element of K10( the U1 of X) : b₁ 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
{ b₁ where b₁ is Element of K10( the U1 of X) : b₁ is (X) } is set
(X) is Element of K10(K10( the U1 of X))
{ b₁ where b₁ is Element of K10( the U1 of X) : Int b₁ = (X,b₁) } 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
{ b₁ where b₁ is Element of K10( the U1 of X) : b₁ 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))
{ b₁ where b₁ is Element of K10( the U1 of X) : Int b₁ = (X,b₁) } 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
{ b₁ where b₁ is Element of K10( the U1 of X) : Int b₁ = (X,b₁) } 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))
{ b₁ where b₁ is Element of K10( the U1 of X) : b₁ 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
{ b₁ where b₁ is Element of K10( the U1 of X) : b₁ is (X) } is set
(X) is Element of K10(K10( the U1 of X))
{ b₁ where b₁ is Element of K10( the U1 of X) : Int b₁ = (X,b₁) } 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))