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