:: TSEP_2 semantic presentation

K87() is set
K10(K87()) is set
K180() is TopStruct
the carrier of K180() is set
{} is set
the empty set is empty set
1 is non empty set
X is non empty 1-sorted
the carrier of X is non empty set
K10( the carrier of X) is set
X0 is Element of K10( the carrier of X)
X0 ` is Element of K10( the carrier of X)
the carrier of X \ X0 is set
X1 is Element of K10( the carrier of X)
X1 ` is Element of K10( the carrier of X)
the carrier of X \ X1 is set
(X0 `) \ (X1 `) is Element of K10( the carrier of X)
X1 \ X0 is Element of K10( the carrier of X)
[#] X is non empty non proper Element of K10( the carrier of X)
X0 \/ (X1 `) is Element of K10( the carrier of X)
([#] X) \ (X0 \/ (X1 `)) is Element of K10( the carrier of X)
(X1 `) ` is Element of K10( the carrier of X)
the carrier of X \ (X1 `) is set
(X0 `) /\ ((X1 `) `) is Element of K10( the carrier of X)
X is 1-sorted
the carrier of X is set
K10( the carrier of X) is set
X2 is Element of K10( the carrier of X)
A1 is Element of K10( the carrier of X)
X2 \/ A1 is Element of K10( the carrier of X)
A1 \/ X2 is Element of K10( the carrier of X)
X is 1-sorted
the carrier of X is set
K10( the carrier of X) is set
X is non empty 1-sorted
the carrier of X is non empty set
K10( the carrier of X) is set
X2 is non empty 1-sorted
the carrier of X2 is non empty set
K10( the carrier of X2) is set
X0 is Element of K10( the carrier of X)
X1 is Element of K10( the carrier of X)
X0 \/ X1 is Element of K10( the carrier of X)
[#] X is non empty non proper Element of K10( the carrier of X)
A1 is Element of K10( the carrier of X2)
A2 is Element of K10( the carrier of X2)
A1 \/ A2 is Element of K10( the carrier of X2)
[#] X2 is non empty non proper Element of K10( the carrier of X2)
X is non empty 1-sorted
the carrier of X is non empty set
K10( the carrier of X) is set
X0 is Element of K10( the carrier of X)
X0 ` is Element of K10( the carrier of X)
the carrier of X \ X0 is set
X1 is Element of K10( the carrier of X)
X1 ` is Element of K10( the carrier of X)
the carrier of X \ X1 is set
X0 \/ X1 is Element of K10( the carrier of X)
[#] X is non empty non proper Element of K10( the carrier of X)
X is non empty 1-sorted
the carrier of X is non empty set
K10( the carrier of X) is set
X0 is Element of K10( the carrier of X)
X0 ` is Element of K10( the carrier of X)
the carrier of X \ X0 is set
X1 is Element of K10( the carrier of X)
X1 ` is Element of K10( the carrier of X)
the carrier of X \ X1 is set
X0 \/ X1 is Element of K10( the carrier of X)
[#] X is non empty non proper Element of K10( the carrier of X)
X is non empty 1-sorted
the carrier of X is non empty set
K10( the carrier of X) is set
X0 is Element of K10( the carrier of X)
X0 ` is Element of K10( the carrier of X)
the carrier of X \ X0 is set
X0 \/ (X0 `) is Element of K10( the carrier of X)
[#] X is non empty non proper Element of K10( the carrier of X)
X is non empty 1-sorted
{} X is empty Element of K10( the carrier of X)
the carrier of X is non empty set
K10( the carrier of X) is set
[#] X is non empty non proper Element of K10( the carrier of X)
({} X) ` is Element of K10( the carrier of X)
the carrier of X \ ({} X) is set
X is non empty 1-sorted
the carrier of X is non empty set
K10( the carrier of X) is set
X0 is Element of K10( the carrier of X)
X0 ` is Element of K10( the carrier of X)
the carrier of X \ X0 is set
X0 /\ X0 is Element of K10( the carrier of X)
X0 \/ X0 is Element of K10( the carrier of X)
X is non empty 1-sorted
the carrier of X is non empty set
K10( the carrier of X) is set
X2 is Element of K10( the carrier of X)
X is non empty 1-sorted
the carrier of X is non empty set
K10( the carrier of X) is set
X0 is Element of K10( the carrier of X)
X1 is Element of K10( the carrier of X)
X2 is Element of K10( the carrier of X)
X1 ` is Element of K10( the carrier of X)
the carrier of X \ X1 is set
X is non empty TopSpace-like TopStruct
the carrier of X is non empty set
K10( the carrier of X) is set
X0 is Element of K10( the carrier of X)
Cl X0 is Element of K10( the carrier of X)
Int X0 is Element of K10( the carrier of X)
X1 is Element of K10( the carrier of X)
Int X1 is Element of K10( the carrier of X)
Cl X1 is Element of K10( the carrier of X)
X0 ` is Element of K10( the carrier of X)
the carrier of X \ X0 is set
Int (X0 `) is Element of K10( the carrier of X)
(Int (X0 `)) ` is Element of K10( the carrier of X)
the carrier of X \ (Int (X0 `)) is set
(Int X1) ` is Element of K10( the carrier of X)
the carrier of X \ (Int X1) is set
Cl (X0 `) is Element of K10( the carrier of X)
(Cl (X0 `)) ` is Element of K10( the carrier of X)
the carrier of X \ (Cl (X0 `)) is set
(Cl X1) ` is Element of K10( the carrier of X)
the carrier of X \ (Cl X1) is set
X is non empty TopSpace-like TopStruct
the carrier of X is non empty set
K10( the carrier of X) is set
X0 is Element of K10( the carrier of X)
Cl X0 is Element of K10( the carrier of X)
X0 ` is Element of K10( the carrier of X)
the carrier of X \ X0 is set
Int (X0 `) is Element of K10( the carrier of X)
Cl (X0 `) is Element of K10( the carrier of X)
Int X0 is Element of K10( the carrier of X)
X is non empty TopSpace-like TopStruct
the carrier of X is non empty set
K10( the carrier of X) is set
X0 is Element of K10( the carrier of X)
X1 is Element of K10( the carrier of X)
X0 ` is Element of K10( the carrier of X)
the carrier of X \ X0 is set
X1 ` is Element of K10( the carrier of X)
the carrier of X \ X1 is set
X is non empty TopSpace-like TopStruct
the carrier of X is non empty set
K10( the carrier of X) is set
X0 is Element of K10( the carrier of X)
X1 is Element of K10( the carrier of X)
X is non empty 1-sorted
the carrier of X is non empty set
K10( the carrier of X) is set
X0 is Element of K10( the carrier of X)
X1 is Element of K10( the carrier of X)
X2 is Element of K10( the carrier of X)
X0 /\ X2 is Element of K10( the carrier of X)
A1 is Element of K10( the carrier of X)
X1 \/ A1 is Element of K10( the carrier of X)
X0 /\ X1 is Element of K10( the carrier of X)
X2 \/ A1 is Element of K10( the carrier of X)
[#] X is non empty non proper Element of K10( the carrier of X)
X2 /\ A1 is Element of K10( the carrier of X)
{} X is empty Element of K10( the carrier of X)
(X0 /\ X2) /\ (X1 \/ A1) is Element of K10( the carrier of X)
X2 /\ X0 is Element of K10( the carrier of X)
(X2 /\ X0) /\ X1 is Element of K10( the carrier of X)
(X0 /\ X2) /\ A1 is Element of K10( the carrier of X)
((X2 /\ X0) /\ X1) \/ ((X0 /\ X2) /\ A1) is Element of K10( the carrier of X)
X2 /\ (X0 /\ X1) is Element of K10( the carrier of X)
(X2 /\ (X0 /\ X1)) \/ ((X0 /\ X2) /\ A1) is Element of K10( the carrier of X)
X0 /\ (X2 /\ A1) is Element of K10( the carrier of X)
(X2 /\ (X0 /\ X1)) \/ (X0 /\ (X2 /\ A1)) is Element of K10( the carrier of X)
(X0 /\ X2) \/ (X1 \/ A1) is Element of K10( the carrier of X)
X0 \/ (X1 \/ A1) is Element of K10( the carrier of X)
X2 \/ (X1 \/ A1) is Element of K10( the carrier of X)
(X0 \/ (X1 \/ A1)) /\ (X2 \/ (X1 \/ A1)) is Element of K10( the carrier of X)
X0 \/ X1 is Element of K10( the carrier of X)
(X0 \/ X1) \/ A1 is Element of K10( the carrier of X)
A1 \/ X1 is Element of K10( the carrier of X)
X2 \/ (A1 \/ X1) is Element of K10( the carrier of X)
((X0 \/ X1) \/ A1) /\ (X2 \/ (A1 \/ X1)) is Element of K10( the carrier of X)
(X2 \/ A1) \/ X1 is Element of K10( the carrier of X)
((X0 \/ X1) \/ A1) /\ ((X2 \/ A1) \/ X1) is Element of K10( the carrier of X)
([#] X) \/ A1 is Element of K10( the carrier of X)
([#] X) \/ X1 is Element of K10( the carrier of X)
(([#] X) \/ A1) /\ (([#] X) \/ X1) is Element of K10( the carrier of X)
(([#] X) \/ A1) /\ ([#] X) is Element of K10( the carrier of X)
([#] X) /\ ([#] X) is Element of K10( the carrier of X)
X is non empty 1-sorted
the carrier of X is non empty set
K10( the carrier of X) is set
X0 is Element of K10( the carrier of X)
X1 is Element of K10( the carrier of X)
X2 is Element of K10( the carrier of X)
A1 is Element of K10( the carrier of X)
X0 \/ X2 is Element of K10( the carrier of X)
X1 /\ A1 is Element of K10( the carrier of X)
X is non empty TopSpace-like TopStruct
the carrier of X is non empty set
K10( the carrier of X) is set
X0 is Element of K10( the carrier of X)
X2 is Element of K10( the carrier of X)
X1 is Element of K10( the carrier of X)
A1 is Element of K10( the carrier of X)
X0 ` is Element of K10( the carrier of X)
the carrier of X \ X0 is set
X1 ` is Element of K10( the carrier of X)
the carrier of X \ X1 is set
X0 \ X1 is Element of K10( the carrier of X)
X1 \ X0 is Element of K10( the carrier of X)
A1 \ X2 is Element of K10( the carrier of X)
A1 ` is Element of K10( the carrier of X)
the carrier of X \ A1 is set
X2 ` is Element of K10( the carrier of X)
the carrier of X \ X2 is set
(A1 `) \ (X2 `) is Element of K10( the carrier of X)
X2 \ A1 is Element of K10( the carrier of X)
X2 \ A1 is Element of K10( the carrier of X)
A1 \ X2 is Element of K10( the carrier of X)
A1 ` is Element of K10( the carrier of X)
the carrier of X \ A1 is set
X2 ` is Element of K10( the carrier of X)
the carrier of X \ X2 is set
(A1 `) \ (X2 `) is Element of K10( the carrier of X)
X1 \ X0 is Element of K10( the carrier of X)
X0 \ X1 is Element of K10( the carrier of X)
X is non empty TopSpace-like TopStruct
the carrier of X is non empty set
K10( the carrier of X) is set
X0 is Element of K10( the carrier of X)
X0 ` is Element of K10( the carrier of X)
the carrier of X \ X0 is set
X1 is Element of K10( the carrier of X)
X1 ` is Element of K10( the carrier of X)
the carrier of X \ X1 is set
X is non empty TopSpace-like TopStruct
the carrier of X is non empty set
K10( the carrier of X) is set
X0 is Element of K10( the carrier of X)
X2 is Element of K10( the carrier of X)
X1 is Element of K10( the carrier of X)
A1 is Element of K10( the carrier of X)
X is non empty TopSpace-like TopStruct
the carrier of X is non empty set
K10( the carrier of X) is set
X0 is Element of K10( the carrier of X)
X2 is Element of K10( the carrier of X)
X1 is Element of K10( the carrier of X)
A1 is Element of K10( the carrier of X)
X0 /\ X1 is Element of K10( the carrier of X)
X is non empty TopSpace-like TopStruct
the carrier of X is non empty set
K10( the carrier of X) is set
X0 is Element of K10( the carrier of X)
X2 is Element of K10( the carrier of X)
X1 is Element of K10( the carrier of X)
A1 is Element of K10( the carrier of X)
X2 \/ A1 is Element of K10( the carrier of X)
(X2 \/ A1) ` is Element of K10( the carrier of X)
the carrier of X \ (X2 \/ A1) is set
{} X is empty closed Element of K10( the carrier of X)
X2 ` is Element of K10( the carrier of X)
the carrier of X \ X2 is set
A1 ` is Element of K10( the carrier of X)
the carrier of X \ A1 is set
X0 /\ X1 is Element of K10( the carrier of X)
X is non empty TopSpace-like TopStruct
the carrier of X is non empty set
K10( the carrier of X) is set
X0 is Element of K10( the carrier of X)
X1 is Element of K10( the carrier of X)
X is non empty TopSpace-like TopStruct
the carrier of X is non empty set
K10( the carrier of X) is set
X0 is Element of K10( the carrier of X)
X1 is Element of K10( the carrier of X)
X0 \/ X1 is Element of K10( the carrier of X)
(X0 \/ X1) \ X0 is Element of K10( the carrier of X)
(X0 \/ X1) \ X1 is Element of K10( the carrier of X)
X1 \ X0 is Element of K10( the carrier of X)
X0 \ X1 is Element of K10( the carrier of X)
X is non empty TopSpace-like TopStruct
the carrier of X is non empty set
K10( the carrier of X) is set
X2 is Element of K10( the carrier of X)
X0 is Element of K10( the carrier of X)
A1 is Element of K10( the carrier of X)
X1 is Element of K10( the carrier of X)
X2 \/ A1 is Element of K10( the carrier of X)
X0 \/ X1 is Element of K10( the carrier of X)
(X0 \/ X1) \ X0 is Element of K10( the carrier of X)
(X0 \/ X1) \ X2 is Element of K10( the carrier of X)
(X0 \/ X1) \ X1 is Element of K10( the carrier of X)
(X0 \/ X1) \ A1 is Element of K10( the carrier of X)
X is non empty TopSpace-like TopStruct
the carrier of X is non empty set
K10( the carrier of X) is set
X0 is Element of K10( the carrier of X)
X1 is Element of K10( the carrier of X)
X0 /\ X1 is Element of K10( the carrier of X)
X0 \ (X0 /\ X1) is Element of K10( the carrier of X)
X1 \ (X0 /\ X1) is Element of K10( the carrier of X)
X1 \ X0 is Element of K10( the carrier of X)
X0 \ X1 is Element of K10( the carrier of X)
X is non empty TopSpace-like TopStruct
the carrier of X is non empty set
K10( the carrier of X) is set
X2 is Element of K10( the carrier of X)
X0 is Element of K10( the carrier of X)
A1 is Element of K10( the carrier of X)
X1 is Element of K10( the carrier of X)
X2 /\ A1 is Element of K10( the carrier of X)
X0 /\ X1 is Element of K10( the carrier of X)
X2 \ (X2 /\ A1) is Element of K10( the carrier of X)
X0 \ (X2 /\ A1) is Element of K10( the carrier of X)
A1 \ (X2 /\ A1) is Element of K10( the carrier of X)
X1 \ (X2 /\ A1) is Element of K10( the carrier of X)
X is non empty TopSpace-like TopStruct
the carrier of X is non empty set
K10( the carrier of X) is set
X0 is Element of K10( the carrier of X)
X1 is Element of K10( the carrier of X)
X2 is non empty TopSpace-like SubSpace of X
the carrier of X2 is non empty set
K10( the carrier of X2) is set
A1 is Element of K10( the carrier of X2)
A2 is Element of K10( the carrier of X2)
Cl A2 is Element of K10( the carrier of X2)
Cl X1 is Element of K10( the carrier of X)
[#] X2 is non empty non proper closed Element of K10( the carrier of X2)
(Cl X1) /\ ([#] X2) is Element of K10( the carrier of X2)
Cl A1 is Element of K10( the carrier of X2)
Cl X0 is Element of K10( the carrier of X)
(Cl X0) /\ ([#] X2) is Element of K10( the carrier of X2)
X0 /\ (Cl X1) is Element of K10( the carrier of X)
A1 /\ (Cl A2) is Element of K10( the carrier of X2)
{} /\ ([#] X2) is Element of K10( the carrier of X2)
(Cl X0) /\ X1 is Element of K10( the carrier of X)
(Cl A1) /\ A2 is Element of K10( the carrier of X2)
((Cl X0) /\ ([#] X2)) /\ X1 is Element of K10( the carrier of X)
(Cl X0) /\ X1 is Element of K10( the carrier of X)
((Cl X0) /\ X1) /\ ([#] X2) is Element of K10( the carrier of X2)
X0 /\ ((Cl X1) /\ ([#] X2)) is Element of K10( the carrier of X2)
X0 /\ (Cl X1) is Element of K10( the carrier of X)
(X0 /\ (Cl X1)) /\ ([#] X2) is Element of K10( the carrier of X2)
X is non empty TopSpace-like TopStruct
the carrier of X is non empty set
K10( the carrier of X) is set
X0 is Element of K10( the carrier of X)
X1 is Element of K10( the carrier of X)
X2 is non empty TopSpace-like SubSpace of X
the carrier of X2 is non empty set
K10( the carrier of X2) is set
the carrier of X2 /\ X0 is Element of K10( the carrier of X)
the carrier of X2 /\ X1 is Element of K10( the carrier of X)
A1 is Element of K10( the carrier of X2)
A2 is Element of K10( the carrier of X2)
Y1 is Element of K10( the carrier of X)
Y2 is Element of K10( the carrier of X)
X is non empty TopSpace-like TopStruct
the carrier of X is non empty set
K10( the carrier of X) is set
X0 is Element of K10( the carrier of X)
X1 is Element of K10( the carrier of X)
X2 is non empty TopSpace-like SubSpace of X
the carrier of X2 is non empty set
K10( the carrier of X2) is set
A1 is Element of K10( the carrier of X2)
A2 is Element of K10( the carrier of X2)
X0 \ X1 is Element of K10( the carrier of X)
X1 \ X0 is Element of K10( the carrier of X)
A1 \ A2 is Element of K10( the carrier of X2)
A2 \ A1 is Element of K10( the carrier of X2)
A1 \ A2 is Element of K10( the carrier of X2)
A2 \ A1 is Element of K10( the carrier of X2)
X0 \ X1 is Element of K10( the carrier of X)
X1 \ X0 is Element of K10( the carrier of X)
X is non empty TopSpace-like TopStruct
the carrier of X is non empty set
K10( the carrier of X) is set
X0 is Element of K10( the carrier of X)
X1 is Element of K10( the carrier of X)
X2 is non empty TopSpace-like SubSpace of X
the carrier of X2 is non empty set
K10( the carrier of X2) is set
the carrier of X2 /\ X0 is Element of K10( the carrier of X)
the carrier of X2 /\ X1 is Element of K10( the carrier of X)
A1 is Element of K10( the carrier of X2)
A2 is Element of K10( the carrier of X2)
A1 \ A2 is Element of K10( the carrier of X2)
X0 \ X1 is Element of K10( the carrier of X)
the carrier of X2 /\ (X0 \ X1) is Element of K10( the carrier of X)
A2 \ A1 is Element of K10( the carrier of X2)
X1 \ X0 is Element of K10( the carrier of X)
the carrier of X2 /\ (X1 \ X0) is Element of K10( the carrier of X)
X is non empty TopSpace-like TopStruct
the carrier of X is non empty set
K10( the carrier of X) is set
X2 is TopSpace-like SubSpace of X
the carrier of X2 is set
A1 is TopSpace-like SubSpace of X
the carrier of A1 is set
A2 is Element of K10( the carrier of X)
Y1 is Element of K10( the carrier of X)
X is non empty TopSpace-like TopStruct
X is non empty TopSpace-like TopStruct
the carrier of X is non empty set
the topology of X is non empty Element of K10(K10( the carrier of X))
K10( the carrier of X) is set
K10(K10( the carrier of X)) is set
TopStruct(# the carrier of X, the topology of X #) is non empty strict TopSpace-like TopStruct
X0 is non empty TopSpace-like SubSpace of X
X1 is non empty TopSpace-like SubSpace of X
X0 union X1 is non empty strict TopSpace-like SubSpace of X
the carrier of X0 is non empty set
the carrier of X1 is non empty set
X2 is Element of K10( the carrier of X)
A1 is Element of K10( the carrier of X)
X2 \/ A1 is Element of K10( the carrier of X)
the carrier of (X0 union X1) is non empty set
A2 is Element of K10( the carrier of X)
Y1 is Element of K10( the carrier of X)
A2 \/ Y1 is Element of K10( the carrier of X)
X is non empty TopSpace-like TopStruct
X0 is non empty TopSpace-like SubSpace of X
the carrier of X is non empty set
K10( the carrier of X) is set
the carrier of X0 is non empty set
X1 is Element of K10( the carrier of X)
X2 is Element of K10( the carrier of X)
A1 is Element of K10( the carrier of X)
X2 is Element of K10( the carrier of X)
A1 is Element of K10( the carrier of X)
X is non empty TopSpace-like TopStruct
X2 is non empty TopSpace-like SubSpace of X
X is non empty TopSpace-like TopStruct
X0 is non empty TopSpace-like SubSpace of X
the carrier of X0 is non empty set
the topology of X0 is non empty Element of K10(K10( the carrier of X0))
K10( the carrier of X0) is set
K10(K10( the carrier of X0)) is set
TopStruct(# the carrier of X0, the topology of X0 #) is non empty strict TopSpace-like TopStruct
X1 is non empty TopSpace-like SubSpace of X
X2 is non empty TopSpace-like SubSpace of X
the carrier of X2 is non empty set
the topology of X2 is non empty Element of K10(K10( the carrier of X2))
K10( the carrier of X2) is set
K10(K10( the carrier of X2)) is set
TopStruct(# the carrier of X2, the topology of X2 #) is non empty strict TopSpace-like TopStruct
the carrier of X is non empty set
K10( the carrier of X) is set
the carrier of X1 is non empty set
A2 is Element of K10( the carrier of X)
A1 is Element of K10( the carrier of X)
Y1 is Element of K10( the carrier of X)
X is non empty TopSpace-like TopStruct
the carrier of X is non empty set
the topology of X is non empty Element of K10(K10( the carrier of X))
K10( the carrier of X) is set
K10(K10( the carrier of X)) is set
TopStruct(# the carrier of X, the topology of X #) is non empty strict TopSpace-like TopStruct
X0 is non empty TopSpace-like SubSpace of X
X2 is non empty TopSpace-like SubSpace of X
X1 is non empty TopSpace-like SubSpace of X
A1 is non empty TopSpace-like SubSpace of X
X2 union A1 is non empty strict TopSpace-like SubSpace of X
the carrier of X0 is non empty set
the carrier of X1 is non empty set
the carrier of X2 is non empty set
the carrier of A1 is non empty set
Y1 is Element of K10( the carrier of X)
C1 is Element of K10( the carrier of X)
C1 ` is Element of K10( the carrier of X)
the carrier of X \ C1 is set
A2 is Element of K10( the carrier of X)
Y2 is Element of K10( the carrier of X)
Y2 ` is Element of K10( the carrier of X)
the carrier of X \ Y2 is set
Y2 \/ C1 is Element of K10( the carrier of X)
(Y2 \/ C1) ` is Element of K10( the carrier of X)
the carrier of X \ (Y2 \/ C1) is set
{} X is empty closed Element of K10( the carrier of X)
A2 /\ Y1 is Element of K10( the carrier of X)
A2 /\ Y1 is Element of K10( the carrier of X)
{} X is empty closed Element of K10( the carrier of X)
Y2 \/ C1 is Element of K10( the carrier of X)
(Y2 \/ C1) ` is Element of K10( the carrier of X)
the carrier of X \ (Y2 \/ C1) is set
({} X) ` is Element of K10( the carrier of X)
the carrier of X \ ({} X) is set
the carrier of (X2 union A1) is non empty set
X is non empty TopSpace-like TopStruct
X0 is non empty TopSpace-like SubSpace of X
X1 is non empty TopSpace-like SubSpace of X
the carrier of X is non empty set
K10( the carrier of X) is set
the carrier of X0 is non empty set
the carrier of X1 is non empty set
A2 is Element of K10( the carrier of X)
X2 is Element of K10( the carrier of X)
A2 is Element of K10( the carrier of X)
A1 is Element of K10( the carrier of X)
X is non empty TopSpace-like TopStruct
X0 is non empty TopSpace-like SubSpace of X
X1 is non empty TopSpace-like SubSpace of X
X is non empty TopSpace-like TopStruct
X0 is non empty TopSpace-like SubSpace of X
X1 is non empty TopSpace-like SubSpace of X
X0 meet X1 is non empty strict TopSpace-like SubSpace of X
X2 is non empty TopSpace-like SubSpace of X
A1 is non empty TopSpace-like SubSpace of X
X2 union A1 is non empty strict TopSpace-like SubSpace of X
the carrier of X is non empty set
K10( the carrier of X) is set
the carrier of X0 is non empty set
the carrier of X2 is non empty set
the carrier of X1 is non empty set
the carrier of A1 is non empty set
A2 is Element of K10( the carrier of X)
Y1 is Element of K10( the carrier of X)
Y2 is Element of K10( the carrier of X)
C1 is Element of K10( the carrier of X)
C2 is Element of K10( the carrier of X)
the carrier of (X0 meet X1) is non empty set
C2 is Element of K10( the carrier of X)
the carrier of (X2 union A1) is non empty set
A2 /\ Y2 is Element of K10( the carrier of X)
Y1 \/ C1 is Element of K10( the carrier of X)
X is non empty TopSpace-like TopStruct
X0 is non empty TopSpace-like SubSpace of X
X1 is non empty TopSpace-like SubSpace of X
X2 is non empty TopSpace-like SubSpace of X
A1 is non empty TopSpace-like SubSpace of X
X2 union A1 is non empty strict TopSpace-like SubSpace of X
X0 meet X1 is non empty strict TopSpace-like SubSpace of X
X is non empty TopSpace-like TopStruct
X0 is TopSpace-like SubSpace of X
X2 is TopSpace-like SubSpace of X
X1 is TopSpace-like SubSpace of X
A1 is TopSpace-like SubSpace of X
the carrier of X is non empty set
K10( the carrier of X) is set
the carrier of X0 is set
the carrier of X2 is set
the carrier of X1 is set
the carrier of A1 is set
Y2 is Element of K10( the carrier of X)
C1 is Element of K10( the carrier of X)
A2 is Element of K10( the carrier of X)
Y1 is Element of K10( the carrier of X)
X is non empty TopSpace-like TopStruct
X0 is non empty TopSpace-like SubSpace of X
X2 is non empty TopSpace-like SubSpace of X
X1 is non empty TopSpace-like SubSpace of X
A1 is non empty TopSpace-like SubSpace of X
X is non empty TopSpace-like TopStruct
X0 is non empty TopSpace-like SubSpace of X
X2 is non empty TopSpace-like SubSpace of X
X1 is non empty TopSpace-like SubSpace of X
A1 is non empty TopSpace-like SubSpace of X
X is non empty TopSpace-like TopStruct
the carrier of X is non empty set
the topology of X is non empty Element of K10(K10( the carrier of X))
K10( the carrier of X) is set
K10(K10( the carrier of X)) is set
TopStruct(# the carrier of X, the topology of X #) is non empty strict TopSpace-like TopStruct
X0 is non empty TopSpace-like SubSpace of X
X2 is non empty TopSpace-like SubSpace of X
X1 is non empty TopSpace-like SubSpace of X
A1 is non empty TopSpace-like SubSpace of X
X2 union A1 is non empty strict TopSpace-like SubSpace of X
X is non empty TopSpace-like TopStruct
X0 is non empty TopSpace-like SubSpace of X
X1 is non empty TopSpace-like SubSpace of X
X is non empty TopSpace-like TopStruct
X2 is non empty TopSpace-like SubSpace of X
X0 is non empty TopSpace-like SubSpace of X
A1 is non empty TopSpace-like SubSpace of X
X1 is non empty TopSpace-like SubSpace of X
X2 union A1 is non empty strict TopSpace-like SubSpace of X
X0 union X1 is non empty strict TopSpace-like SubSpace of X
the carrier of X is non empty set
K10( the carrier of X) is set
the carrier of X0 is non empty set
the carrier of X1 is non empty set
the carrier of X2 is non empty set
the carrier of A1 is non empty set
Y2 is Element of K10( the carrier of X)
A2 is Element of K10( the carrier of X)
C1 is Element of K10( the carrier of X)
Y1 is Element of K10( the carrier of X)
C2 is Element of K10( the carrier of X)
C2 is Element of K10( the carrier of X)
C2 \/ C2 is Element of K10( the carrier of X)
the carrier of (X0 union X1) is non empty set
Y2 \/ C1 is Element of K10( the carrier of X)
X is non empty TopSpace-like TopStruct
X2 is non empty TopSpace-like SubSpace of X
X0 is non empty TopSpace-like SubSpace of X
A1 is non empty TopSpace-like SubSpace of X
X1 is non empty TopSpace-like SubSpace of X
X2 meet A1 is non empty strict TopSpace-like SubSpace of X
X0 meet X1 is non empty strict TopSpace-like SubSpace of X
the carrier of X is non empty set
K10( the carrier of X) is set
the carrier of X0 is non empty set
the carrier of X1 is non empty set
the carrier of X2 is non empty set
the carrier of A1 is non empty set
Y2 is Element of K10( the carrier of X)
A2 is Element of K10( the carrier of X)
C1 is Element of K10( the carrier of X)
Y1 is Element of K10( the carrier of X)
C2 is Element of K10( the carrier of X)
C2 is Element of K10( the carrier of X)
C2 /\ C2 is Element of K10( the carrier of X)
A2 /\ Y1 is Element of K10( the carrier of X)
the carrier of (X0 meet X1) is non empty set
X is non empty TopSpace-like TopStruct
X0 is non empty TopSpace-like SubSpace of X
X1 is TopSpace-like SubSpace of X
the carrier of X1 is set
X2 is TopSpace-like SubSpace of X
the carrier of X2 is set
A1 is TopSpace-like SubSpace of X0
the carrier of A1 is set
A2 is TopSpace-like SubSpace of X0
the carrier of A2 is set
the carrier of X is non empty set
K10( the carrier of X) is set
the carrier of X0 is non empty set
K10( the carrier of X0) is set
Y1 is Element of K10( the carrier of X)
Y2 is Element of K10( the carrier of X)
C2 is Element of K10( the carrier of X0)
c₁₂ is Element of K10( the carrier of X0)
C1 is Element of K10( the carrier of X0)
C2 is Element of K10( the carrier of X0)
C2 is Element of K10( the carrier of X)
c₁₂ is Element of K10( the carrier of X)
X is non empty TopSpace-like TopStruct
X0 is non empty TopSpace-like SubSpace of X
X1 is non empty TopSpace-like SubSpace of X
X2 is non empty TopSpace-like SubSpace of X
X1 meet X0 is non empty strict TopSpace-like SubSpace of X
X2 meet X0 is non empty strict TopSpace-like SubSpace of X
A1 is TopSpace-like SubSpace of X0
A2 is TopSpace-like SubSpace of X0
X is non empty TopSpace-like TopStruct
X0 is non empty TopSpace-like SubSpace of X
X1 is TopSpace-like SubSpace of X
the carrier of X1 is set
X2 is TopSpace-like SubSpace of X
the carrier of X2 is set
A1 is TopSpace-like SubSpace of X0
the carrier of A1 is set
A2 is TopSpace-like SubSpace of X0
the carrier of A2 is set
the carrier of X is non empty set
K10( the carrier of X) is set
the carrier of X0 is non empty set
K10( the carrier of X0) is set
Y1 is Element of K10( the carrier of X)
Y2 is Element of K10( the carrier of X)
C2 is Element of K10( the carrier of X0)
c₁₂ is Element of K10( the carrier of X0)
C1 is Element of K10( the carrier of X0)
C2 is Element of K10( the carrier of X0)
C2 is Element of K10( the carrier of X)
c₁₂ is Element of K10( the carrier of X)
X is non empty TopSpace-like TopStruct
X0 is non empty TopSpace-like SubSpace of X
X1 is non empty TopSpace-like SubSpace of X
X2 is non empty TopSpace-like SubSpace of X
X1 meet X0 is non empty strict TopSpace-like SubSpace of X
X2 meet X0 is non empty strict TopSpace-like SubSpace of X
the carrier of X is non empty set
K10( the carrier of X) is set
the carrier of X1 is non empty set
the carrier of X2 is non empty set
Y1 is TopSpace-like SubSpace of X0
Y2 is TopSpace-like SubSpace of X0
A1 is Element of K10( the carrier of X)
A2 is Element of K10( the carrier of X)
the carrier of X0 is non empty set
K10( the carrier of X0) is set
C1 is Element of K10( the carrier of X0)
the carrier of Y1 is set
C2 is Element of K10( the carrier of X0)
the carrier of Y2 is set
the carrier of X0 /\ A1 is Element of K10( the carrier of X)
the carrier of X0 /\ A2 is Element of K10( the carrier of X)