:: TOPS_3 semantic presentation

K87() is set

K10(K87()) is set

K179() is non empty strict TopSpace-like TopStruct

the carrier of K179() is non empty set

{} is set

the empty set is empty set

1 is non empty set

X1 is TopStruct

the carrier of X1 is set

K10( the carrier of X1) is set

{} X1 is empty boundary Element of K10( the carrier of X1)

[#] X1 is non proper dense Element of K10( the carrier of X1)

X2 is Element of K10( the carrier of X1)

X2 ` is Element of K10( the carrier of X1)

the carrier of X1 \ X2 is set

(X2 `) ` is Element of K10( the carrier of X1)

the carrier of X1 \ (X2 `) is set

X1 is TopStruct

the carrier of X1 is set

K10( the carrier of X1) is set

[#] X1 is non proper dense Element of K10( the carrier of X1)

{} X1 is empty boundary Element of K10( the carrier of X1)

X2 is Element of K10( the carrier of X1)

X2 ` is Element of K10( the carrier of X1)

the carrier of X1 \ X2 is set

(X2 `) ` is Element of K10( the carrier of X1)

the carrier of X1 \ (X2 `) is set

X1 is TopSpace-like TopStruct

the carrier of X1 is set

K10( the carrier of X1) is set

X2 is Element of K10( the carrier of X1)

Int X2 is open Element of K10( the carrier of X1)

D1 is Element of K10( the carrier of X1)

Cl D1 is closed Element of K10( the carrier of X1)

(Int X2) /\ (Cl D1) is Element of K10( the carrier of X1)

X2 /\ D1 is Element of K10( the carrier of X1)

Cl (X2 /\ D1) is closed Element of K10( the carrier of X1)

(Int X2) /\ D1 is Element of K10( the carrier of X1)

Cl ((Int X2) /\ D1) is closed Element of K10( the carrier of X1)

X1 is TopSpace-like TopStruct

the carrier of X1 is set

K10( the carrier of X1) is set

X2 is Element of K10( the carrier of X1)

Cl X2 is closed Element of K10( the carrier of X1)

D1 is Element of K10( the carrier of X1)

X2 \/ D1 is Element of K10( the carrier of X1)

Int (X2 \/ D1) is open Element of K10( the carrier of X1)

Int D1 is open Element of K10( the carrier of X1)

(Cl X2) \/ (Int D1) is Element of K10( the carrier of X1)

X2 ` is Element of K10( the carrier of X1)

the carrier of X1 \ X2 is set

Int (X2 `) is open Element of K10( the carrier of X1)

D1 ` is Element of K10( the carrier of X1)

the carrier of X1 \ D1 is set

Cl (D1 `) is closed Element of K10( the carrier of X1)

(Int (X2 `)) /\ (Cl (D1 `)) is Element of K10( the carrier of X1)

(X2 `) /\ (D1 `) is Element of K10( the carrier of X1)

Cl ((X2 `) /\ (D1 `)) is closed Element of K10( the carrier of X1)

(Cl ((X2 `) /\ (D1 `))) ` is open Element of K10( the carrier of X1)

the carrier of X1 \ (Cl ((X2 `) /\ (D1 `))) is set

((Int (X2 `)) /\ (Cl (D1 `))) ` is Element of K10( the carrier of X1)

the carrier of X1 \ ((Int (X2 `)) /\ (Cl (D1 `))) is set

((X2 `) /\ (D1 `)) ` is Element of K10( the carrier of X1)

the carrier of X1 \ ((X2 `) /\ (D1 `)) is set

Int (((X2 `) /\ (D1 `)) `) is open Element of K10( the carrier of X1)

(X2 `) ` is Element of K10( the carrier of X1)

the carrier of X1 \ (X2 `) is set

(D1 `) ` is Element of K10( the carrier of X1)

the carrier of X1 \ (D1 `) is set

((X2 `) `) \/ ((D1 `) `) is Element of K10( the carrier of X1)

Int (((X2 `) `) \/ ((D1 `) `)) is open Element of K10( the carrier of X1)

(Int (X2 `)) ` is closed Element of K10( the carrier of X1)

the carrier of X1 \ (Int (X2 `)) is set

(Cl (D1 `)) ` is open Element of K10( the carrier of X1)

the carrier of X1 \ (Cl (D1 `)) is set

((Int (X2 `)) `) \/ ((Cl (D1 `)) `) is Element of K10( the carrier of X1)

(Cl X2) \/ ((Cl (D1 `)) `) is Element of K10( the carrier of X1)

X1 is TopSpace-like TopStruct

the carrier of X1 is set

K10( the carrier of X1) is set

X2 is Element of K10( the carrier of X1)

Int X2 is open Element of K10( the carrier of X1)

D1 is Element of K10( the carrier of X1)

D1 \/ X2 is Element of K10( the carrier of X1)

Int (D1 \/ X2) is open Element of K10( the carrier of X1)

D1 \/ (Int X2) is Element of K10( the carrier of X1)

Cl D1 is closed Element of K10( the carrier of X1)

X1 is TopSpace-like TopStruct

the carrier of X1 is set

K10( the carrier of X1) is set

X2 is Element of K10( the carrier of X1)

Int X2 is open Element of K10( the carrier of X1)

D1 is Element of K10( the carrier of X1)

D1 \/ X2 is Element of K10( the carrier of X1)

Int (D1 \/ X2) is open Element of K10( the carrier of X1)

D1 \/ (Int X2) is Element of K10( the carrier of X1)

Int (D1 \/ (Int X2)) is open Element of K10( the carrier of X1)

Int (Int (D1 \/ X2)) is open Element of K10( the carrier of X1)

X1 is TopSpace-like TopStruct

the carrier of X1 is set

K10( the carrier of X1) is set

X2 is Element of K10( the carrier of X1)

Cl X2 is closed Element of K10( the carrier of X1)

Int (Cl X2) is open Element of K10( the carrier of X1)

X2 /\ (Int (Cl X2)) is Element of K10( the carrier of X1)

D1 is Element of K10( the carrier of X1)

Cl D1 is closed Element of K10( the carrier of X1)

Int (Cl D1) is open Element of K10( the carrier of X1)

(Cl X2) /\ (Int (Cl X2)) is Element of K10( the carrier of X1)

X1 is TopSpace-like TopStruct

the carrier of X1 is set

K10( the carrier of X1) is set

X2 is Element of K10( the carrier of X1)

Int X2 is open Element of K10( the carrier of X1)

Cl (Int X2) is closed Element of K10( the carrier of X1)

X2 \/ (Cl (Int X2)) is Element of K10( the carrier of X1)

(Int X2) \/ (Cl (Int X2)) is Element of K10( the carrier of X1)

X1 is TopStruct

the carrier of X1 is set

K10( the carrier of X1) is set

X2 is Element of K10( the carrier of X1)

Int X2 is Element of K10( the carrier of X1)

X1 is TopSpace-like TopStruct

{} X1 is empty open closed boundary nowhere_dense Element of K10( the carrier of X1)

the carrier of X1 is set

K10( the carrier of X1) is set

X1 is non empty TopSpace-like TopStruct

the carrier of X1 is non empty set

K10( the carrier of X1) is set

X2 is Element of K10( the carrier of X1)

Int X2 is open Element of K10( the carrier of X1)

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

X1 is TopSpace-like TopStruct

the carrier of X1 is set

K10( the carrier of X1) is set

X2 is Element of K10( the carrier of X1)

D1 is Element of K10( the carrier of X1)

Int X2 is open Element of K10( the carrier of X1)

Int D1 is open Element of K10( the carrier of X1)

X1 is TopSpace-like TopStruct

the carrier of X1 is set

K10( the carrier of X1) is set

X2 is Element of K10( the carrier of X1)

X2 ` is Element of K10( the carrier of X1)

the carrier of X1 \ X2 is set

D1 is Element of K10( the carrier of X1)

D1 ` is Element of K10( the carrier of X1)

the carrier of X1 \ D1 is set

(X2 `) ` is Element of K10( the carrier of X1)

the carrier of X1 \ (X2 `) is set

{} X1 is empty open closed boundary nowhere_dense Element of K10( the carrier of X1)

D1 is Element of K10( the carrier of X1)

D1 ` is Element of K10( the carrier of X1)

the carrier of X1 \ D1 is set

X1 is TopSpace-like TopStruct

the carrier of X1 is set

K10( the carrier of X1) is set

X2 is Element of K10( the carrier of X1)

X2 ` is Element of K10( the carrier of X1)

the carrier of X1 \ X2 is set

D1 is Element of K10( the carrier of X1)

Int X2 is open Element of K10( the carrier of X1)

X1 is TopSpace-like TopStruct

the carrier of X1 is set

K10( the carrier of X1) is set

X2 is Element of K10( the carrier of X1)

Int X2 is open Element of K10( the carrier of X1)

D1 is Element of K10( the carrier of X1)

Int D1 is open Element of K10( the carrier of X1)

D1 \/ X2 is Element of K10( the carrier of X1)

Int (D1 \/ X2) is open Element of K10( the carrier of X1)

D1 \/ (Int X2) is Element of K10( the carrier of X1)

Int (D1 \/ (Int X2)) is open Element of K10( the carrier of X1)

{} X1 is empty open closed boundary nowhere_dense Element of K10( the carrier of X1)

Int ({} X1) is empty open closed boundary nowhere_dense Element of K10( the carrier of X1)

({} X1) \/ X2 is Element of K10( the carrier of X1)

Int (({} X1) \/ X2) is open Element of K10( the carrier of X1)

X1 is TopSpace-like TopStruct

the carrier of X1 is set

K10( the carrier of X1) is set

X2 is Element of K10( the carrier of X1)

D1 is Element of K10( the carrier of X1)

X2 /\ D1 is Element of K10( the carrier of X1)

X1 is TopStruct

the carrier of X1 is set

K10( the carrier of X1) is set

X2 is Element of K10( the carrier of X1)

Cl X2 is Element of K10( the carrier of X1)

[#] X1 is non proper dense Element of K10( the carrier of X1)

[#] X1 is non proper dense Element of K10( the carrier of X1)

X1 is TopSpace-like TopStruct

[#] X1 is non proper open closed dense Element of K10( the carrier of X1)

the carrier of X1 is set

K10( the carrier of X1) is set

X1 is non empty TopSpace-like TopStruct

the carrier of X1 is non empty set

K10( the carrier of X1) is set

X2 is Element of K10( the carrier of X1)

Cl X2 is closed Element of K10( the carrier of X1)

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

X1 is non empty TopSpace-like TopStruct

the carrier of X1 is non empty set

K10( the carrier of X1) is set

X2 is Element of K10( the carrier of X1)

X2 ` is Element of K10( the carrier of X1)

the carrier of X1 \ X2 is set

(X2 `) ` is Element of K10( the carrier of X1)

the carrier of X1 \ (X2 `) is set

(X2 `) ` is Element of K10( the carrier of X1)

the carrier of X1 \ (X2 `) is set

X1 is non empty TopSpace-like TopStruct

the carrier of X1 is non empty set

K10( the carrier of X1) is set

X2 is Element of K10( the carrier of X1)

Cl X2 is closed Element of K10( the carrier of X1)

D1 is Element of K10( the carrier of X1)

Cl X2 is closed Element of K10( the carrier of X1)

X1 is non empty TopSpace-like TopStruct

the carrier of X1 is non empty set

K10( the carrier of X1) is set

X2 is Element of K10( the carrier of X1)

D1 is Element of K10( the carrier of X1)

Cl D1 is closed Element of K10( the carrier of X1)

D1 /\ X2 is Element of K10( the carrier of X1)

Cl (D1 /\ X2) is closed Element of K10( the carrier of X1)

Cl X2 is closed Element of K10( the carrier of X1)

D1 /\ (Cl X2) is Element of K10( the carrier of X1)

Cl (D1 /\ (Cl X2)) is closed Element of K10( the carrier of X1)

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

D1 /\ ([#] X1) is Element of K10( the carrier of X1)

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

Cl ([#] X1) is closed Element of K10( the carrier of X1)

([#] X1) /\ X2 is Element of K10( the carrier of X1)

Cl (([#] X1) /\ X2) is closed Element of K10( the carrier of X1)

X1 is non empty TopSpace-like TopStruct

the carrier of X1 is non empty set

K10( the carrier of X1) is set

X2 is Element of K10( the carrier of X1)

D1 is Element of K10( the carrier of X1)

X2 \/ D1 is Element of K10( the carrier of X1)

X1 is TopStruct

the carrier of X1 is set

K10( the carrier of X1) is set

X2 is Element of K10( the carrier of X1)

Cl X2 is Element of K10( the carrier of X1)

Int (Cl X2) is Element of K10( the carrier of X1)

X1 is non empty TopSpace-like TopStruct

{} X1 is empty open closed boundary nowhere_dense Element of K10( the carrier of X1)

the carrier of X1 is non empty set

K10( the carrier of X1) is set

X1 is non empty TopSpace-like TopStruct

the carrier of X1 is non empty set

K10( the carrier of X1) is set

X2 is Element of K10( the carrier of X1)

X1 is non empty TopSpace-like TopStruct

the carrier of X1 is non empty set

K10( the carrier of X1) is set

X2 is Element of K10( the carrier of X1)

Cl X2 is closed Element of K10( the carrier of X1)

X1 is non empty TopSpace-like TopStruct

the carrier of X1 is non empty set

K10( the carrier of X1) is set

X2 is Element of K10( the carrier of X1)

Cl X2 is closed Element of K10( the carrier of X1)

Int (Cl X2) is open Element of K10( the carrier of X1)

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

X1 is non empty TopSpace-like TopStruct

the carrier of X1 is non empty set

K10( the carrier of X1) is set

X2 is Element of K10( the carrier of X1)

D1 is Element of K10( the carrier of X1)

Cl X2 is closed Element of K10( the carrier of X1)

Cl D1 is closed Element of K10( the carrier of X1)

X1 is non empty TopSpace-like TopStruct

the carrier of X1 is non empty set

K10( the carrier of X1) is set

X2 is Element of K10( the carrier of X1)

Cl X2 is closed Element of K10( the carrier of X1)

D1 is Element of K10( the carrier of X1)

Cl X2 is closed Element of K10( the carrier of X1)

X1 is non empty TopSpace-like TopStruct

the carrier of X1 is non empty set

K10( the carrier of X1) is set

X2 is Element of K10( the carrier of X1)

Cl X2 is closed Element of K10( the carrier of X1)

D1 is Element of K10( the carrier of X1)

D2 is Element of K10( the carrier of X1)

Cl X2 is closed Element of K10( the carrier of X1)

D1 is Element of K10( the carrier of X1)

D2 is Element of K10( the carrier of X1)

X1 is non empty TopSpace-like TopStruct

the carrier of X1 is non empty set

K10( the carrier of X1) is set

X2 is Element of K10( the carrier of X1)

D1 is Element of K10( the carrier of X1)

X2 /\ D1 is Element of K10( the carrier of X1)

X1 is non empty TopSpace-like TopStruct

the carrier of X1 is non empty set

K10( the carrier of X1) is set

X2 is Element of K10( the carrier of X1)

D1 is Element of K10( the carrier of X1)

X2 \/ D1 is Element of K10( the carrier of X1)

Cl X2 is closed Element of K10( the carrier of X1)

D1 \/ (Cl X2) is Element of K10( the carrier of X1)

X1 is TopStruct

the carrier of X1 is set

K10( the carrier of X1) is set

X1 is TopStruct

the carrier of X1 is set

K10( the carrier of X1) is set

X2 is Element of K10( the carrier of X1)

Int X2 is Element of K10( the carrier of X1)

Cl (Int X2) is Element of K10( the carrier of X1)

[#] X1 is non proper dense Element of K10( the carrier of X1)

[#] X1 is non proper dense Element of K10( the carrier of X1)

X1 is non empty TopSpace-like TopStruct

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

the carrier of X1 is non empty set

K10( the carrier of X1) is set

Int ([#] X1) is open Element of K10( the carrier of X1)

Cl (Int ([#] X1)) is closed Element of K10( the carrier of X1)

X1 is non empty TopSpace-like TopStruct

the carrier of X1 is non empty set

K10( the carrier of X1) is set

X2 is Element of K10( the carrier of X1)

Int X2 is open Element of K10( the carrier of X1)

Int (Int X2) is open Element of K10( the carrier of X1)

Cl (Int (Int X2)) is closed Element of K10( the carrier of X1)

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

X1 is non empty TopSpace-like TopStruct

the carrier of X1 is non empty set

K10( the carrier of X1) is set

X2 is Element of K10( the carrier of X1)

Int X2 is open Element of K10( the carrier of X1)

Cl (Int X2) is closed Element of K10( the carrier of X1)

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

Cl X2 is closed Element of K10( the carrier of X1)

X1 is non empty TopSpace-like TopStruct

the carrier of X1 is non empty set

K10( the carrier of X1) is set

X2 is Element of K10( the carrier of X1)

X1 is non empty TopSpace-like TopStruct

the carrier of X1 is non empty set

K10( the carrier of X1) is set

X2 is Element of K10( the carrier of X1)

Int X2 is open Element of K10( the carrier of X1)

Cl (Int X2) is closed Element of K10( the carrier of X1)

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

X1 is non empty TopSpace-like TopStruct

the carrier of X1 is non empty set

K10( the carrier of X1) is set

X2 is Element of K10( the carrier of X1)

Int X2 is open Element of K10( the carrier of X1)

X1 is non empty TopSpace-like TopStruct

the carrier of X1 is non empty set

K10( the carrier of X1) is set

X2 is Element of K10( the carrier of X1)

Int X2 is open Element of K10( the carrier of X1)

Cl (Int X2) is closed Element of K10( the carrier of X1)

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

X1 is non empty TopSpace-like TopStruct

the carrier of X1 is non empty set

K10( the carrier of X1) is set

X2 is Element of K10( the carrier of X1)

D1 is Element of K10( the carrier of X1)

Int X2 is open Element of K10( the carrier of X1)

Cl (Int X2) is closed Element of K10( the carrier of X1)

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

Int D1 is open Element of K10( the carrier of X1)

Cl (Int D1) is closed Element of K10( the carrier of X1)

X1 is non empty TopSpace-like TopStruct

the carrier of X1 is non empty set

K10( the carrier of X1) is set

X2 is Element of K10( the carrier of X1)

X2 ` is Element of K10( the carrier of X1)

the carrier of X1 \ X2 is set

Int X2 is open Element of K10( the carrier of X1)

Cl (Int X2) is closed Element of K10( the carrier of X1)

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

(Cl (Int X2)) ` is open Element of K10( the carrier of X1)

the carrier of X1 \ (Cl (Int X2)) is set

{} X1 is empty open closed boundary nowhere_dense Element of K10( the carrier of X1)

(Int X2) ` is closed Element of K10( the carrier of X1)

the carrier of X1 \ (Int X2) is set

Int ((Int X2) `) is open Element of K10( the carrier of X1)

Cl (X2 `) is closed Element of K10( the carrier of X1)

Int (Cl (X2 `)) is open Element of K10( the carrier of X1)

Cl (X2 `) is closed Element of K10( the carrier of X1)

Int (Cl (X2 `)) is open Element of K10( the carrier of X1)

{} X1 is empty open closed boundary nowhere_dense Element of K10( the carrier of X1)

Int X2 is open Element of K10( the carrier of X1)

(Int X2) ` is closed Element of K10( the carrier of X1)

the carrier of X1 \ (Int X2) is set

Int ((Int X2) `) is open Element of K10( the carrier of X1)

Cl (Int X2) is closed Element of K10( the carrier of X1)

(Cl (Int X2)) ` is open Element of K10( the carrier of X1)

the carrier of X1 \ (Cl (Int X2)) is set

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

X1 is non empty TopSpace-like TopStruct

the carrier of X1 is non empty set

K10( the carrier of X1) is set

X2 is Element of K10( the carrier of X1)

X2 ` is Element of K10( the carrier of X1)

the carrier of X1 \ X2 is set

Cl X2 is closed Element of K10( the carrier of X1)

Int (Cl X2) is open Element of K10( the carrier of X1)

{} X1 is empty open closed boundary nowhere_dense Element of K10( the carrier of X1)

Int (X2 `) is open Element of K10( the carrier of X1)

(Int (X2 `)) ` is closed Element of K10( the carrier of X1)

the carrier of X1 \ (Int (X2 `)) is set

Int ((Int (X2 `)) `) is open Element of K10( the carrier of X1)

Cl (Int (X2 `)) is closed Element of K10( the carrier of X1)

(Cl (Int (X2 `))) ` is open Element of K10( the carrier of X1)

the carrier of X1 \ (Cl (Int (X2 `))) is set

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

Int (X2 `) is open Element of K10( the carrier of X1)

Cl (Int (X2 `)) is closed Element of K10( the carrier of X1)

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

(Cl (Int (X2 `))) ` is open Element of K10( the carrier of X1)

the carrier of X1 \ (Cl (Int (X2 `))) is set

{} X1 is empty open closed boundary nowhere_dense Element of K10( the carrier of X1)

(Int (X2 `)) ` is closed Element of K10( the carrier of X1)

the carrier of X1 \ (Int (X2 `)) is set

Int ((Int (X2 `)) `) is open Element of K10( the carrier of X1)

Cl X2 is closed Element of K10( the carrier of X1)

Int (Cl X2) is open Element of K10( the carrier of X1)

X1 is non empty TopSpace-like TopStruct

the carrier of X1 is non empty set

K10( the carrier of X1) is set

X2 is Element of K10( the carrier of X1)

Int X2 is open Element of K10( the carrier of X1)

D1 is Element of K10( the carrier of X1)

Int X2 is open Element of K10( the carrier of X1)

X1 is non empty TopSpace-like TopStruct

the carrier of X1 is non empty set

K10( the carrier of X1) is set

X2 is Element of K10( the carrier of X1)

X2 ` is Element of K10( the carrier of X1)

the carrier of X1 \ X2 is set

D1 is Element of K10( the carrier of X1)

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

([#] X1) \ D1 is Element of K10( the carrier of X1)

D1 ` is Element of K10( the carrier of X1)

the carrier of X1 \ D1 is set

D2 is Element of K10( the carrier of X1)

D2 ` is Element of K10( the carrier of X1)

the carrier of X1 \ D2 is set

C2 is Element of K10( the carrier of X1)

X2 \/ C2 is Element of K10( the carrier of X1)

(D1 `) ` is Element of K10( the carrier of X1)

the carrier of X1 \ (D1 `) is set

C2 ` is Element of K10( the carrier of X1)

the carrier of X1 \ C2 is set

([#] X1) \ C2 is Element of K10( the carrier of X1)

(X2 `) /\ (C2 `) is Element of K10( the carrier of X1)

(X2 \/ C2) ` is Element of K10( the carrier of X1)

the carrier of X1 \ (X2 \/ C2) is set

{} X1 is empty open closed boundary nowhere_dense Element of K10( the carrier of X1)

X2 ` is Element of K10( the carrier of X1)

the carrier of X1 \ X2 is set

D1 is Element of K10( the carrier of X1)

D1 ` is Element of K10( the carrier of X1)

the carrier of X1 \ D1 is set

(D1 `) ` is Element of K10( the carrier of X1)

the carrier of X1 \ (D1 `) is set

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

D2 is Element of K10( the carrier of X1)

X2 \/ D2 is Element of K10( the carrier of X1)

D2 ` is Element of K10( the carrier of X1)

the carrier of X1 \ D2 is set

C2 is Element of K10( the carrier of X1)

(X2 \/ D2) ` is Element of K10( the carrier of X1)

the carrier of X1 \ (X2 \/ D2) is set

{} X1 is empty open closed boundary nowhere_dense Element of K10( the carrier of X1)

(X2 `) /\ C2 is Element of K10( the carrier of X1)

X1 is non empty TopSpace-like TopStruct

the carrier of X1 is non empty set

K10( the carrier of X1) is set

X2 is Element of K10( the carrier of X1)

D1 is Element of K10( the carrier of X1)

X2 \/ D1 is Element of K10( the carrier of X1)

X1 is non empty TopSpace-like TopStruct

the carrier of X1 is non empty set

K10( the carrier of X1) is set

X2 is Element of K10( the carrier of X1)

D1 is Element of K10( the carrier of X1)

X2 /\ D1 is Element of K10( the carrier of X1)

X2 ` is Element of K10( the carrier of X1)

the carrier of X1 \ X2 is set

D1 ` is Element of K10( the carrier of X1)

the carrier of X1 \ D1 is set

(X2 `) \/ (D1 `) is Element of K10( the carrier of X1)

(X2 /\ D1) ` is Element of K10( the carrier of X1)

the carrier of X1 \ (X2 /\ D1) is set

X1 is non empty TopSpace-like TopStruct

the carrier of X1 is non empty set

K10( the carrier of X1) is set

X2 is Element of K10( the carrier of X1)

D1 is Element of K10( the carrier of X1)

X2 /\ D1 is Element of K10( the carrier of X1)

X2 ` is Element of K10( the carrier of X1)

the carrier of X1 \ X2 is set

D1 ` is Element of K10( the carrier of X1)

the carrier of X1 \ D1 is set

(X2 `) \/ (D1 `) is Element of K10( the carrier of X1)

(X2 /\ D1) ` is Element of K10( the carrier of X1)

the carrier of X1 \ (X2 /\ D1) is set

X1 is non empty TopSpace-like TopStruct

the carrier of X1 is non empty set

K10( the carrier of X1) is set

X2 is Element of K10( the carrier of X1)

D1 is Element of K10( the carrier of X1)

X2 \ D1 is Element of K10( the carrier of X1)

D1 ` is Element of K10( the carrier of X1)

the carrier of X1 \ D1 is set

(D1 `) /\ X2 is Element of K10( the carrier of X1)

X1 is non empty TopSpace-like TopStruct

the carrier of X1 is non empty set

K10( the carrier of X1) is set

X2 is Element of K10( the carrier of X1)

D1 is Element of K10( the carrier of X1)

X2 \ D1 is Element of K10( the carrier of X1)

D1 ` is Element of K10( the carrier of X1)

the carrier of X1 \ D1 is set

X2 /\ (D1 `) is Element of K10( the carrier of X1)

X1 is non empty TopSpace-like TopStruct

the carrier of X1 is non empty set

K10( the carrier of X1) is set

X2 is Element of K10( the carrier of X1)

D1 is Element of K10( the carrier of X1)

X2 \ D1 is Element of K10( the carrier of X1)

D1 ` is Element of K10( the carrier of X1)

the carrier of X1 \ D1 is set

X2 /\ (D1 `) is Element of K10( the carrier of X1)

X1 is non empty TopSpace-like TopStruct

the carrier of X1 is non empty set

K10( the carrier of X1) is set

X2 is Element of K10( the carrier of X1)

D1 is Element of K10( the carrier of X1)

X2 \ D1 is Element of K10( the carrier of X1)

D2 is Element of K10( the carrier of X1)

D1 \/ D2 is Element of K10( the carrier of X1)

D1 ` is Element of K10( the carrier of X1)

the carrier of X1 \ D1 is set

X1 is non empty TopSpace-like TopStruct

the carrier of X1 is non empty set

K10( the carrier of X1) is set

X2 is Element of K10( the carrier of X1)

D1 is Element of K10( the carrier of X1)

D1 ` is Element of K10( the carrier of X1)

the carrier of X1 \ D1 is set

D2 is Element of K10( the carrier of X1)

X2 /\ D2 is Element of K10( the carrier of X1)

D1 \/ (X2 /\ D2) is Element of K10( the carrier of X1)

D1 \/ D2 is Element of K10( the carrier of X1)

D1 \/ X2 is Element of K10( the carrier of X1)

D1 \/ (D1 `) is Element of K10( the carrier of X1)

(D1 \/ X2) /\ (D1 \/ (D1 `)) is Element of K10( the carrier of X1)

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

(D1 \/ X2) /\ ([#] X1) is Element of K10( the carrier of X1)

D1 /\ D2 is Element of K10( the carrier of X1)

X1 is non empty TopSpace-like TopStruct

the carrier of X1 is non empty set

K10( the carrier of X1) is set

X2 is Element of K10( the carrier of X1)

D1 is Element of K10( the carrier of X1)

D1 ` is Element of K10( the carrier of X1)

the carrier of X1 \ D1 is set

X2 \/ (D1 `) is Element of K10( the carrier of X1)

D2 is Element of K10( the carrier of X1)

D1 /\ D2 is Element of K10( the carrier of X1)

D1 \/ D2 is Element of K10( the carrier of X1)

D1 /\ X2 is Element of K10( the carrier of X1)

D1 /\ (D1 `) is Element of K10( the carrier of X1)

(D1 /\ X2) \/ (D1 /\ (D1 `)) is Element of K10( the carrier of X1)

{} X1 is empty open closed boundary nowhere_dense Element of K10( the carrier of X1)

(D1 /\ X2) \/ ({} X1) is Element of K10( the carrier of X1)

D1 \/ (D1 `) is Element of K10( the carrier of X1)

X2 \/ (D1 \/ (D1 `)) is Element of K10( the carrier of X1)

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

X2 \/ ([#] X1) is Element of K10( the carrier of X1)

X1 is non empty TopSpace-like TopStruct

the carrier of X1 is non empty set

K10( the carrier of X1) is set

X2 is Element of K10( the carrier of X1)

D1 is Element of K10( the carrier of X1)

D1 ` is Element of K10( the carrier of X1)

the carrier of X1 \ D1 is set

D2 is Element of K10( the carrier of X1)

X2 \/ D2 is Element of K10( the carrier of X1)

D1 /\ (X2 \/ D2) is Element of K10( the carrier of X1)

D1 \/ D2 is Element of K10( the carrier of X1)

D1 /\ X2 is Element of K10( the carrier of X1)

D1 /\ (D1 `) is Element of K10( the carrier of X1)

(D1 /\ X2) \/ (D1 /\ (D1 `)) is Element of K10( the carrier of X1)

{} X1 is empty open closed boundary nowhere_dense Element of K10( the carrier of X1)

(D1 /\ X2) \/ ({} X1) is Element of K10( the carrier of X1)

D1 /\ D2 is Element of K10( the carrier of X1)

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

X1 is non empty TopSpace-like TopStruct

the carrier of X1 is non empty set

K10( the carrier of X1) is set

X2 is TopSpace-like SubSpace of X1

the carrier of X2 is set

K10( the carrier of X2) is set

D1 is Element of K10( the carrier of X1)

Cl D1 is closed Element of K10( the carrier of X1)

D2 is Element of K10( the carrier of X2)

Cl D2 is closed Element of K10( the carrier of X2)

C2 is Element of K10( the carrier of X1)

Cl C2 is closed Element of K10( the carrier of X1)

[#] X2 is non proper open closed dense Element of K10( the carrier of X2)

(Cl C2) /\ ([#] X2) is Element of K10( the carrier of X2)

X1 is non empty TopSpace-like TopStruct

the carrier of X1 is non empty set

K10( the carrier of X1) is set

X2 is TopSpace-like SubSpace of X1

the carrier of X2 is set

K10( the carrier of X2) is set

D1 is Element of K10( the carrier of X1)

D2 is Element of K10( the carrier of X1)

Cl D2 is closed Element of K10( the carrier of X1)

C2 is Element of K10( the carrier of X2)

Cl C2 is closed Element of K10( the carrier of X2)

Cl D1 is closed Element of K10( the carrier of X1)

[#] X2 is non proper open closed dense Element of K10( the carrier of X2)

(Cl D2) /\ ([#] X2) is Element of K10( the carrier of X2)

X1 is non empty TopSpace-like TopStruct

the carrier of X1 is non empty set

K10( the carrier of X1) is set

X2 is non empty TopSpace-like closed SubSpace of X1

the carrier of X2 is non empty set

K10( the carrier of X2) is set

D2 is Element of K10( the carrier of X1)

Cl D2 is closed Element of K10( the carrier of X1)

C2 is Element of K10( the carrier of X2)

Cl C2 is closed Element of K10( the carrier of X2)

D1 is Element of K10( the carrier of X1)

X1 is non empty TopSpace-like TopStruct

the carrier of X1 is non empty set

K10( the carrier of X1) is set

X2 is TopSpace-like SubSpace of X1

the carrier of X2 is set

K10( the carrier of X2) is set

D1 is Element of K10( the carrier of X1)

Int D1 is open Element of K10( the carrier of X1)

D2 is Element of K10( the carrier of X2)

Int D2 is open Element of K10( the carrier of X2)

C2 is Element of K10( the carrier of X2)

X1 is non empty TopSpace-like TopStruct

the carrier of X1 is non empty set

K10( the carrier of X1) is set

X2 is non empty TopSpace-like SubSpace of X1

the carrier of X2 is non empty set

K10( the carrier of X2) is set

D1 is Element of K10( the carrier of X1)

D2 is Element of K10( the carrier of X1)

Int D2 is open Element of K10( the carrier of X1)

C2 is Element of K10( the carrier of X2)

Int C2 is open Element of K10( the carrier of X2)

C1 is Element of K10( the carrier of X1)

X1 is non empty TopSpace-like TopStruct

the carrier of X1 is non empty set

K10( the carrier of X1) is set

X2 is non empty TopSpace-like open SubSpace of X1

the carrier of X2 is non empty set

K10( the carrier of X2) is set

D2 is Element of K10( the carrier of X1)

Int D2 is open Element of K10( the carrier of X1)

C2 is Element of K10( the carrier of X2)

Int C2 is open Element of K10( the carrier of X2)

D1 is Element of K10( the carrier of X1)

X1 is non empty TopSpace-like TopStruct

the carrier of X1 is non empty set

K10( the carrier of X1) is set

X2 is TopSpace-like SubSpace of X1

the carrier of X2 is set

K10( the carrier of X2) is set

D1 is Element of K10( the carrier of X1)

D2 is Element of K10( the carrier of X2)

[#] X2 is non proper open closed dense Element of K10( the carrier of X2)

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

Cl D1 is closed Element of K10( the carrier of X1)

(Cl D1) /\ ([#] X2) is Element of K10( the carrier of X2)

C2 is Element of K10( the carrier of X2)

Cl C2 is closed Element of K10( the carrier of X2)

X1 is non empty TopSpace-like TopStruct

the carrier of X1 is non empty set

K10( the carrier of X1) is set

X2 is TopSpace-like SubSpace of X1

the carrier of X2 is set

K10( the carrier of X2) is set

D1 is Element of K10( the carrier of X1)

D2 is Element of K10( the carrier of X1)

C2 is Element of K10( the carrier of X2)

Cl D1 is closed Element of K10( the carrier of X1)

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

C1 is Element of K10( the carrier of X1)

Cl C1 is closed Element of K10( the carrier of X1)

Cl C2 is closed Element of K10( the carrier of X2)

[#] X2 is non proper open closed dense Element of K10( the carrier of X2)

Cl D2 is closed Element of K10( the carrier of X1)

(Cl D2) /\ ([#] X2) is Element of K10( the carrier of X2)

Cl (Cl D2) is closed Element of K10( the carrier of X1)

X1 is non empty TopSpace-like TopStruct

the carrier of X1 is non empty set

K10( the carrier of X1) is set

X2 is non empty TopSpace-like SubSpace of X1

the carrier of X2 is non empty set

K10( the carrier of X2) is set

D1 is Element of K10( the carrier of X1)

D2 is Element of K10( the carrier of X2)

Int D1 is open Element of K10( the carrier of X1)

C2 is Element of K10( the carrier of X2)

Int C2 is open Element of K10( the carrier of X2)

Int D2 is open Element of K10( the carrier of X2)

X1 is non empty TopSpace-like TopStruct

the carrier of X1 is non empty set

K10( the carrier of X1) is set

X2 is non empty TopSpace-like SubSpace of X1

the carrier of X2 is non empty set

K10( the carrier of X2) is set

D1 is Element of K10( the carrier of X1)

D2 is Element of K10( the carrier of X1)

C2 is Element of K10( the carrier of X2)

C1 is Element of K10( the carrier of X2)

Int C2 is open Element of K10( the carrier of X2)

Int C1 is open Element of K10( the carrier of X2)

E is Element of K10( the carrier of X1)

Int D2 is open Element of K10( the carrier of X1)

X1 is non empty TopSpace-like TopStruct

the carrier of X1 is non empty set

K10( the carrier of X1) is set

X2 is non empty TopSpace-like open SubSpace of X1

the carrier of X2 is non empty set

K10( the carrier of X2) is set

D2 is Element of K10( the carrier of X1)

D1 is Element of K10( the carrier of X1)

C2 is Element of K10( the carrier of X2)

X1 is non empty TopSpace-like TopStruct

the carrier of X1 is non empty set

K10( the carrier of X1) is set

X2 is non empty TopSpace-like SubSpace of X1

the carrier of X2 is non empty set

K10( the carrier of X2) is set

D1 is Element of K10( the carrier of X1)

D2 is Element of K10( the carrier of X1)

C2 is Element of K10( the carrier of X2)

Int D1 is open Element of K10( the carrier of X1)

C1 is Element of K10( the carrier of X2)

C1 /\ C2 is Element of K10( the carrier of X2)

E is Element of K10( the carrier of X1)

X1 is non empty TopSpace-like TopStruct

the carrier of X1 is non empty set

K10( the carrier of X1) is set

X2 is non empty TopSpace-like SubSpace of X1

the carrier of X2 is non empty set

K10( the carrier of X2) is set

D1 is Element of K10( the carrier of X1)

D2 is Element of K10( the carrier of X2)

Int D2 is open Element of K10( the carrier of X2)

C2 is Element of K10( the carrier of X2)

Int C2 is open Element of K10( the carrier of X2)

Int D1 is open Element of K10( the carrier of X1)

X1 is non empty TopSpace-like TopStruct

the carrier of X1 is non empty set

K10( the carrier of X1) is set

X2 is non empty TopSpace-like SubSpace of X1

the carrier of X2 is non empty set

K10( the carrier of X2) is set

D1 is Element of K10( the carrier of X1)

D2 is Element of K10( the carrier of X1)

C2 is Element of K10( the carrier of X2)

Int D2 is open Element of K10( the carrier of X1)

Int C2 is open Element of K10( the carrier of X2)

X1 is non empty TopSpace-like TopStruct

the carrier of X1 is non empty set

K10( the carrier of X1) is set

X2 is non empty TopSpace-like open SubSpace of X1

the carrier of X2 is non empty set

K10( the carrier of X2) is set

D1 is Element of K10( the carrier of X1)

D2 is Element of K10( the carrier of X2)

C2 is Element of K10( the carrier of X1)

X1 is non empty TopSpace-like TopStruct

the carrier of X1 is non empty set

K10( the carrier of X1) is set

X2 is non empty TopSpace-like SubSpace of X1

the carrier of X2 is non empty set

K10( the carrier of X2) is set

D1 is Element of K10( the carrier of X1)

D2 is Element of K10( the carrier of X2)

Cl D1 is closed Element of K10( the carrier of X1)

Int (Cl D1) is open Element of K10( the carrier of X1)

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

(Int (Cl D1)) /\ ([#] X2) is Element of K10( the carrier of X2)

E is Element of K10( the carrier of X2)

C1 is Element of K10( the carrier of X2)

Cl E is closed Element of K10( the carrier of X2)

Int (Cl E) is open Element of K10( the carrier of X2)

(Cl D1) /\ ([#] X2) is Element of K10( the carrier of X2)

D1 /\ (Int (Cl D1)) is Element of K10( the carrier of X1)

C2 is Element of K10( the carrier of X1)

(Int (Cl D1)) /\ C2 is Element of K10( the carrier of X1)

X1 is non empty TopSpace-like TopStruct

the carrier of X1 is non empty set

K10( the carrier of X1) is set

X2 is non empty TopSpace-like SubSpace of X1

the carrier of X2 is non empty set

K10( the carrier of X2) is set

D1 is Element of K10( the carrier of X1)

D2 is Element of K10( the carrier of X1)

C2 is Element of K10( the carrier of X2)

Cl C2 is closed Element of K10( the carrier of X2)

Cl D2 is closed Element of K10( the carrier of X1)

Int (Cl D2) is open Element of K10( the carrier of X1)

C1 is Element of K10( the carrier of X1)

Int C1 is open Element of K10( the carrier of X1)

Int (Cl C2) is open Element of K10( the carrier of X2)

X1 is non empty TopSpace-like TopStruct

the carrier of X1 is non empty set

K10( the carrier of X1) is set

X2 is non empty TopSpace-like SubSpace of X1

the carrier of X2 is non empty set

K10( the carrier of X2) is set

D1 is Element of K10( the carrier of X1)

D2 is Element of K10( the carrier of X1)

C2 is Element of K10( the carrier of X2)

C1 is non empty strict TopSpace-like SubSpace of X1

the carrier of C1 is non empty set

K10( the carrier of C1) is set

E is Element of K10( the carrier of C1)

{} X2 is empty open closed boundary nowhere_dense Element of K10( the carrier of X2)

X1 is non empty TopSpace-like TopStruct

the carrier of X1 is non empty set

K10( the carrier of X1) is set

X2 is non empty TopSpace-like open SubSpace of X1

the carrier of X2 is non empty set

K10( the carrier of X2) is set

D1 is Element of K10( the carrier of X1)

D2 is Element of K10( the carrier of X2)

C2 is Element of K10( the carrier of X1)

X1 is 1-sorted

the carrier of X1 is set

X2 is 1-sorted

the carrier of X2 is set

K10( the carrier of X1) is set

K10( the carrier of X2) is set

D1 is Element of K10( the carrier of X1)

D1 ` is Element of K10( the carrier of X1)

the carrier of X1 \ D1 is set

D2 is Element of K10( the carrier of X2)

D2 ` is Element of K10( the carrier of X2)

the carrier of X2 \ D2 is set

[#] X2 is non proper Element of K10( the carrier of X2)

([#] X2) \ (D2 `) is Element of K10( the carrier of X2)

X1 is TopStruct

the carrier of X1 is set

K10( the carrier of X1) is set

the topology of X1 is Element of K10(K10( the carrier of X1))

K10(K10( the carrier of X1)) is set

TopStruct(# the carrier of X1, the topology of X1 #) is strict TopStruct

X2 is TopStruct

the carrier of X2 is set

K10( the carrier of X2) is set

the topology of X2 is Element of K10(K10( the carrier of X2))

K10(K10( the carrier of X2)) is set

TopStruct(# the carrier of X2, the topology of X2 #) is strict TopStruct

D1 is set

D2 is Element of K10( the carrier of X2)

C2 is Element of K10( the carrier of X1)

D1 is set

D2 is Element of K10( the carrier of X1)

C2 is Element of K10( the carrier of X2)

X1 is TopStruct

the carrier of X1 is set

K10( the carrier of X1) is set

the topology of X1 is Element of K10(K10( the carrier of X1))

K10(K10( the carrier of X1)) is set

TopStruct(# the carrier of X1, the topology of X1 #) is strict TopStruct

X2 is TopStruct

the carrier of X2 is set

K10( the carrier of X2) is set

the topology of X2 is Element of K10(K10( the carrier of X2))

K10(K10( the carrier of X2)) is set

TopStruct(# the carrier of X2, the topology of X2 #) is strict TopStruct

D1 is Element of K10( the carrier of X1)

D2 is Element of K10( the carrier of X2)

D1 ` is Element of K10( the carrier of X1)

the carrier of X1 \ D1 is set

D2 ` is Element of K10( the carrier of X2)

the carrier of X2 \ D2 is set

D2 ` is Element of K10( the carrier of X2)

the carrier of X2 \ D2 is set

D1 ` is Element of K10( the carrier of X1)

the carrier of X1 \ D1 is set

X1 is TopSpace-like TopStruct

the carrier of X1 is set

K10( the carrier of X1) is set

the topology of X1 is non empty Element of K10(K10( the carrier of X1))

K10(K10( the carrier of X1)) is set

TopStruct(# the carrier of X1, the topology of X1 #) is strict TopSpace-like TopStruct

X2 is TopSpace-like TopStruct

the carrier of X2 is set

K10( the carrier of X2) is set

the topology of X2 is non empty Element of K10(K10( the carrier of X2))

K10(K10( the carrier of X2)) is set

TopStruct(# the carrier of X2, the topology of X2 #) is strict TopSpace-like TopStruct

D1 is Element of K10( the carrier of X1)

D2 is Element of K10( the carrier of X2)

Int D1 is open Element of K10( the carrier of X1)

Int D2 is open Element of K10( the carrier of X2)

Int D2 is open Element of K10( the carrier of X2)

Int D1 is open Element of K10( the carrier of X1)

X1 is TopSpace-like TopStruct

the carrier of X1 is set

K10( the carrier of X1) is set

the topology of X1 is non empty Element of K10(K10( the carrier of X1))

K10(K10( the carrier of X1)) is set

TopStruct(# the carrier of X1, the topology of X1 #) is strict TopSpace-like TopStruct

X2 is TopSpace-like TopStruct

the carrier of X2 is set

K10( the carrier of X2) is set

the topology of X2 is non empty Element of K10(K10( the carrier of X2))

K10(K10( the carrier of X2)) is set

TopStruct(# the carrier of X2, the topology of X2 #) is strict TopSpace-like TopStruct

D1 is Element of K10( the carrier of X1)

D2 is Element of K10( the carrier of X2)

Cl D1 is closed Element of K10( the carrier of X1)

Cl D2 is closed Element of K10( the carrier of X2)

Cl D2 is closed Element of K10( the carrier of X2)

Cl D1 is closed Element of K10( the carrier of X1)

X1 is TopSpace-like TopStruct

the carrier of X1 is set

K10( the carrier of X1) is set

the topology of X1 is non empty Element of K10(K10( the carrier of X1))

K10(K10( the carrier of X1)) is set

TopStruct(# the carrier of X1, the topology of X1 #) is strict TopSpace-like TopStruct

X2 is TopSpace-like TopStruct

the carrier of X2 is set

K10( the carrier of X2) is set

the topology of X2 is non empty Element of K10(K10( the carrier of X2))

K10(K10( the carrier of X2)) is set

TopStruct(# the carrier of X2, the topology of X2 #) is strict TopSpace-like TopStruct

D1 is Element of K10( the carrier of X1)

D2 is Element of K10( the carrier of X2)

X1 is TopSpace-like TopStruct

the carrier of X1 is set

K10( the carrier of X1) is set

the topology of X1 is non empty Element of K10(K10( the carrier of X1))

K10(K10( the carrier of X1)) is set

TopStruct(# the carrier of X1, the topology of X1 #) is strict TopSpace-like TopStruct

X2 is TopSpace-like TopStruct

the carrier of X2 is set

K10( the carrier of X2) is set

the topology of X2 is non empty Element of K10(K10( the carrier of X2))

K10(K10( the carrier of X2)) is set

TopStruct(# the carrier of X2, the topology of X2 #) is strict TopSpace-like TopStruct

D1 is Element of K10( the carrier of X1)

Int D1 is open Element of K10( the carrier of X1)

D2 is Element of K10( the carrier of X2)

Int D2 is open Element of K10( the carrier of X2)

C2 is Element of K10( the carrier of X2)

C1 is Element of K10( the carrier of X1)

X1 is TopSpace-like TopStruct

the carrier of X1 is set

K10( the carrier of X1) is set

the topology of X1 is non empty Element of K10(K10( the carrier of X1))

K10(K10( the carrier of X1)) is set

TopStruct(# the carrier of X1, the topology of X1 #) is strict TopSpace-like TopStruct

X2 is TopSpace-like TopStruct

the carrier of X2 is set

K10( the carrier of X2) is set

the topology of X2 is non empty Element of K10(K10( the carrier of X2))

K10(K10( the carrier of X2)) is set

TopStruct(# the carrier of X2, the topology of X2 #) is strict TopSpace-like TopStruct

D1 is Element of K10( the carrier of X1)

Int D1 is open Element of K10( the carrier of X1)

D2 is Element of K10( the carrier of X2)

Int D2 is open Element of K10( the carrier of X2)

C2 is Element of K10( the carrier of X2)

Int C2 is open Element of K10( the carrier of X2)

X1 is TopSpace-like TopStruct

the carrier of X1 is set

K10( the carrier of X1) is set

the topology of X1 is non empty Element of K10(K10( the carrier of X1))

K10(K10( the carrier of X1)) is set

TopStruct(# the carrier of X1, the topology of X1 #) is strict TopSpace-like TopStruct

X2 is TopSpace-like TopStruct

the carrier of X2 is set

K10( the carrier of X2) is set

the topology of X2 is non empty Element of K10(K10( the carrier of X2))

K10(K10( the carrier of X2)) is set

TopStruct(# the carrier of X2, the topology of X2 #) is strict TopSpace-like TopStruct

D1 is Element of K10( the carrier of X1)

D2 is Element of K10( the carrier of X2)

D2 ` is Element of K10( the carrier of X2)

the carrier of X2 \ D2 is set

X1 is TopSpace-like TopStruct

the carrier of X1 is set

K10( the carrier of X1) is set

the topology of X1 is non empty Element of K10(K10( the carrier of X1))

K10(K10( the carrier of X1)) is set

TopStruct(# the carrier of X1, the topology of X1 #) is strict TopSpace-like TopStruct

X2 is TopSpace-like TopStruct

the carrier of X2 is set

K10( the carrier of X2) is set

the topology of X2 is non empty Element of K10(K10( the carrier of X2))

K10(K10( the carrier of X2)) is set

TopStruct(# the carrier of X2, the topology of X2 #) is strict TopSpace-like TopStruct

D1 is Element of K10( the carrier of X1)

Cl D1 is closed Element of K10( the carrier of X1)

D2 is Element of K10( the carrier of X2)

Cl D2 is closed Element of K10( the carrier of X2)

C2 is Element of K10( the carrier of X2)

C1 is Element of K10( the carrier of X1)

X1 is TopSpace-like TopStruct

the carrier of X1 is set

K10( the carrier of X1) is set

the topology of X1 is non empty Element of K10(K10( the carrier of X1))

K10(K10( the carrier of X1)) is set

TopStruct(# the carrier of X1, the topology of X1 #) is strict TopSpace-like TopStruct

X2 is TopSpace-like TopStruct

the carrier of X2 is set

K10( the carrier of X2) is set

the topology of X2 is non empty Element of K10(K10( the carrier of X2))

K10(K10( the carrier of X2)) is set

TopStruct(# the carrier of X2, the topology of X2 #) is strict TopSpace-like TopStruct

D1 is Element of K10( the carrier of X1)

Cl D1 is closed Element of K10( the carrier of X1)

D2 is Element of K10( the carrier of X2)

Cl D2 is closed Element of K10( the carrier of X2)

C2 is Element of K10( the carrier of X2)

Cl C2 is closed Element of K10( the carrier of X2)

X1 is TopSpace-like TopStruct

the carrier of X1 is set

K10( the carrier of X1) is set

the topology of X1 is non empty Element of K10(K10( the carrier of X1))

K10(K10( the carrier of X1)) is set

TopStruct(# the carrier of X1, the topology of X1 #) is strict TopSpace-like TopStruct

X2 is TopSpace-like TopStruct

the carrier of X2 is set

K10( the carrier of X2) is set

the topology of X2 is non empty Element of K10(K10( the carrier of X2))

K10(K10( the carrier of X2)) is set

TopStruct(# the carrier of X2, the topology of X2 #) is strict TopSpace-like TopStruct

D1 is Element of K10( the carrier of X1)

D2 is Element of K10( the carrier of X2)

C2 is Element of K10( the carrier of X1)

Int C2 is open Element of K10( the carrier of X1)

Int D2 is open Element of K10( the carrier of X2)

X1 is TopSpace-like TopStruct

the carrier of X1 is set

K10( the carrier of X1) is set

the topology of X1 is non empty Element of K10(K10( the carrier of X1))

K10(K10( the carrier of X1)) is set

TopStruct(# the carrier of X1, the topology of X1 #) is strict TopSpace-like TopStruct

X2 is TopSpace-like TopStruct

the carrier of X2 is set

K10( the carrier of X2) is set

the topology of X2 is non empty Element of K10(K10( the carrier of X2))

K10(K10( the carrier of X2)) is set

TopStruct(# the carrier of X2, the topology of X2 #) is strict TopSpace-like TopStruct

D1 is Element of K10( the carrier of X1)

D2 is Element of K10( the carrier of X2)

Cl D1 is closed Element of K10( the carrier of X1)

C2 is Element of K10( the carrier of X2)

Cl C2 is closed Element of K10( the carrier of X2)

X1 is TopSpace-like TopStruct

the carrier of X1 is set

K10( the carrier of X1) is set

the topology of X1 is non empty Element of K10(K10( the carrier of X1))

K10(K10( the carrier of X1)) is set

TopStruct(# the carrier of X1, the topology of X1 #) is strict TopSpace-like TopStruct

X2 is TopSpace-like TopStruct

the carrier of X2 is set

K10( the carrier of X2) is set

the topology of X2 is non empty Element of K10(K10( the carrier of X2))

K10(K10( the carrier of X2)) is set

TopStruct(# the carrier of X2, the topology of X2 #) is strict TopSpace-like TopStruct

D1 is Element of K10( the carrier of X1)

D2 is Element of K10( the carrier of X2)

Cl D1 is closed Element of K10( the carrier of X1)

Cl D2 is closed Element of K10( the carrier of X2)

X1 is non empty TopSpace-like TopStruct

the carrier of X1 is non empty set

K10( the carrier of X1) is set

the topology of X1 is non empty Element of K10(K10( the carrier of X1))

K10(K10( the carrier of X1)) is set

TopStruct(# the carrier of X1, the topology of X1 #) is non empty strict TopSpace-like TopStruct

X2 is non empty TopSpace-like TopStruct

the carrier of X2 is non empty set

K10( the carrier of X2) is set

the topology of X2 is non empty Element of K10(K10( the carrier of X2))

K10(K10( the carrier of X2)) is set

TopStruct(# the carrier of X2, the topology of X2 #) is non empty strict TopSpace-like TopStruct

D1 is Element of K10( the carrier of X1)

D2 is Element of K10( the carrier of X2)

Int D1 is open Element of K10( the carrier of X1)

Int D2 is open Element of K10( the carrier of X2)