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

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

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

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

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)