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

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

{ b

{ b

{ b

{ b

{ b

{ b

{ b

{ b

{ b

{ b

{ b

{ b

{ b

{ b

{ b

{ b

{ b

{ b

{ b

{ b

{ b

{ b

{ b

{ b

{ b

{ b

{ b

{ b

{ b

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

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

{ b

(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

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

{ b

(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

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

{ b

(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

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

{ b

(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

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

{ b

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

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

{ b

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

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

{ b

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

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

{ b

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

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

{ b

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

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

{ b

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

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

{ b

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

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

{ b

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

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

{ b

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

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

{ b

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

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

{ b

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

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

{ b

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

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

{ b

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

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

{ b

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

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

{ b

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

{ b

(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

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

{ b

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

{ b

(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

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

{ b

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

{ b

(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

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

{ b

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

{ b

(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

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

{ b

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

{ b

(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

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

{ b

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

{ b

(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

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

{ b

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

{ b

(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

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

{ b

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

{ b

(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

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

{ b

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

{ b

(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

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

{ b

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

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

{ b

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

{ b

(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

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

{ b

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

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

{ b

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

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

{ b

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

{ b

(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

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

{ b

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

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

{ b

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

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

{ b

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

{ b

(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

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

{ b

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

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

{ b

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

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

{ b

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

{ b

(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

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

{ b

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

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

(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

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

(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

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

{ b

(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

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

(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

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

(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

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

{ b

(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

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

(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

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

(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

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

{ b

(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

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

(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

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

(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

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

{ b

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