:: TSEP_1 semantic presentation

K87() is set

K10(K87()) is set

K178() is non empty strict TopSpace-like TopStruct

the carrier of K178() is non empty set

{} is empty set

1 is non empty set

T is set

K10(T) is set

X1 is Element of K10(T)

X2 is Element of K10(T)

X1 \ X2 is Element of K10(T)

Y1 is Element of K10(T)

Y1 \ X2 is Element of K10(T)

T is set

X1 is set

T /\ X1 is set

X2 is set

(T /\ X1) \ X2 is Element of K10((T /\ X1))

K10((T /\ X1)) is set

T \ X2 is Element of K10(T)

K10(T) is set

X1 \ X2 is Element of K10(X1)

K10(X1) is set

(T \ X2) /\ (X1 \ X2) is Element of K10(X1)

(T \ X2) /\ X1 is Element of K10(T)

(T \ X2) \ X1 is Element of K10(T)

(T \ X2) \ ((T \ X2) \ X1) is Element of K10(T)

X2 \/ X1 is set

T \ (X2 \/ X1) is Element of K10(T)

(T \ X2) \ (T \ (X2 \/ X1)) is Element of K10(T)

(T \ X2) \ T is Element of K10(T)

(T \ X2) /\ (X2 \/ X1) is Element of K10(T)

((T \ X2) \ T) \/ ((T \ X2) /\ (X2 \/ X1)) is Element of K10(T)

{} \/ ((T \ X2) /\ (X2 \/ X1)) is set

(X1 \ X2) \/ X2 is set

(T \ X2) /\ ((X1 \ X2) \/ X2) is Element of K10(T)

(T \ X2) /\ X2 is Element of K10(T)

((T \ X2) /\ (X1 \ X2)) \/ ((T \ X2) /\ X2) is set

((T \ X2) /\ (X1 \ X2)) \/ {} is set

T is TopStruct

the carrier of T is set

K10( the carrier of T) is set

X1 is SubSpace of T

the carrier of X1 is set

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

K10(([#] T)) is set

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

K10( the carrier of X1) is set

X2 is Element of K10(([#] T))

T is TopStruct

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

the carrier of T is set

K10( the carrier of T) is set

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

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

X1 is Element of K10( the carrier of T)

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

X2 is Element of K10( the carrier of T)

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

T is strict TopStruct

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

the carrier of T is set

K10( the carrier of T) is set

T | ([#] T) is strict SubSpace of T

X1 is SubSpace of T

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

the carrier of X1 is set

K10( the carrier of X1) is set

X2 is Element of K10( the carrier of T)

T | X2 is strict SubSpace of T

T is TopSpace-like TopStruct

X1 is TopSpace-like SubSpace of T

the carrier of X1 is set

X2 is TopSpace-like SubSpace of T

the carrier of X2 is set

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

K10( the carrier of X1) is set

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

K10( the carrier of X2) 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

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

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

C2 is Element of K10( the carrier of X1)

the carrier of T is set

K10( the carrier of T) is set

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

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

C1 is Element of K10( the carrier of T)

C1 /\ the carrier of X1 is Element of K10( the carrier of T)

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

A1 is Element of K10( the carrier of X2)

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

the carrier of X2 /\ the carrier of X1 is set

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

C1 is Element of K10( the carrier of X2)

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

the carrier of T is set

K10( the carrier of T) is set

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

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

A1 is Element of K10( the carrier of T)

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

the carrier of X2 /\ the carrier of X1 is set

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

A1 /\ the carrier of X1 is Element of K10( the carrier of T)

T is TopStruct

X1 is SubSpace of T

the carrier of X1 is set

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

K10( the carrier of X1) is set

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

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

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

[#] TopStruct(# the carrier of X1, the topology of X1 #) is non proper Element of K10( the carrier of TopStruct(# the carrier of X1, the topology of X1 #))

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

K10( the carrier of TopStruct(# the carrier of X1, the topology of X1 #)) is set

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

the carrier of T is set

K10( the carrier of T) is set

the topology of TopStruct(# the carrier of X1, the topology of X1 #) is Element of K10(K10( the carrier of TopStruct(# the carrier of X1, the topology of X1 #)))

K10(K10( the carrier of TopStruct(# the carrier of X1, the topology of X1 #))) is set

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

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

Y1 is Element of K10( the carrier of TopStruct(# the carrier of X1, the topology of X1 #))

Y2 is Element of K10( the carrier of T)

Y2 /\ ([#] TopStruct(# the carrier of X1, the topology of X1 #)) is Element of K10( the carrier of TopStruct(# the carrier of X1, the topology of X1 #))

T is TopStruct

X1 is SubSpace of T

the carrier of X1 is set

X2 is SubSpace of T

the carrier of X2 is set

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

K10( the carrier of X1) is set

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

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

the topology of X2 is 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 strict TopStruct

Y1 is strict SubSpace of T

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

the carrier of Y1 is set

K10( the carrier of Y1) is set

Y2 is strict SubSpace of T

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

the carrier of Y2 is set

K10( the carrier of Y2) is set

the carrier of T is set

K10( the carrier of T) is set

A1 is Element of K10( the carrier of T)

T | A1 is strict SubSpace of T

T is TopSpace-like TopStruct

X1 is TopSpace-like SubSpace of T

X2 is TopSpace-like SubSpace of T

the carrier of X1 is set

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

K10( the carrier of X1) is set

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

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

the carrier of X2 is 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 strict TopSpace-like TopStruct

T is TopSpace-like TopStruct

X1 is TopSpace-like SubSpace of T

X2 is TopSpace-like SubSpace of X1

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

the carrier of X2 is set

K10( the carrier of X2) is set

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

the carrier of X1 is set

K10( the carrier of X1) is set

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

the carrier of T is set

K10( the carrier of T) 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

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

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

Y1 is Element of K10( the carrier of X2)

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

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

C2 is Element of K10( the carrier of X1)

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

C1 is Element of K10( the carrier of T)

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

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

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

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

C2 is Element of K10( the carrier of T)

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

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

A1 is Element of K10( the carrier of T)

C1 is Element of K10( the carrier of X1)

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

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

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

Y2 is Element of K10( the carrier of X2)

T is TopSpace-like TopStruct

the carrier of T is set

K10( the carrier of T) is set

X1 is TopSpace-like SubSpace of T

the carrier of X1 is set

K10( the carrier of X1) is set

X2 is Element of K10( the carrier of T)

Y1 is Element of K10( the carrier of T)

Y2 is Element of K10( the carrier of X1)

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

C2 is Element of K10( the carrier of T)

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

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

T is TopSpace-like TopStruct

the carrier of T is set

K10( the carrier of T) is set

X1 is TopSpace-like SubSpace of T

the carrier of X1 is set

K10( the carrier of X1) is set

X2 is Element of K10( the carrier of T)

Y1 is Element of K10( the carrier of T)

Y2 is Element of K10( the carrier of X1)

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

C2 is Element of K10( the carrier of T)

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

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

T is non empty TopStruct

the carrier of T is non empty set

K10( the carrier of T) is set

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

T | X1 is non empty strict SubSpace of T

X2 is non empty strict SubSpace of T

the carrier of X2 is non empty set

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

K10( the carrier of X2) is set

T is TopSpace-like TopStruct

the carrier of T is set

K10( the carrier of T) is set

X1 is TopSpace-like SubSpace of T

the carrier of X1 is set

X2 is Element of K10( the carrier of T)

Y1 is Element of K10( the carrier of T)

T is TopSpace-like TopStruct

the carrier of T is set

K10( the carrier of T) is set

X1 is TopSpace-like closed SubSpace of T

the carrier of X1 is set

K10( the carrier of X1) is set

X2 is Element of K10( the carrier of T)

Y1 is Element of K10( the carrier of X1)

Y2 is Element of K10( the carrier of T)

T is TopSpace-like TopStruct

X1 is TopSpace-like closed SubSpace of T

X2 is TopSpace-like closed SubSpace of X1

the carrier of T is set

K10( the carrier of T) is set

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

the carrier of X1 is set

K10( the carrier of X1) is set

Y2 is Element of K10( the carrier of T)

the carrier of X2 is set

C2 is Element of K10( the carrier of X1)

Y1 is Element of K10( the carrier of T)

C1 is Element of K10( the carrier of T)

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

T is non empty TopSpace-like TopStruct

X1 is non empty TopSpace-like closed SubSpace of T

the carrier of X1 is non empty set

X2 is non empty TopSpace-like SubSpace of T

the carrier of X2 is non empty set

K10( the carrier of X2) is set

Y2 is Element of K10( the carrier of X2)

the carrier of T is non empty set

K10( the carrier of T) is set

C2 is Element of K10( the carrier of T)

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

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

Y1 is Element of K10( the carrier of X2)

T is non empty TopSpace-like TopStruct

the carrier of T is non empty set

K10( the carrier of T) is set

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

X2 is non empty strict TopSpace-like SubSpace of T

the carrier of X2 is non empty set

Y1 is non empty strict TopSpace-like closed SubSpace of T

the carrier of Y1 is non empty set

T is TopStruct

T is TopStruct

the carrier of T is set

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

K10( the carrier of T) is set

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

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

[#] TopStruct(# the carrier of T, the topology of T #) is non proper Element of K10( the carrier of TopStruct(# the carrier of T, the topology of T #))

the carrier of TopStruct(# the carrier of T, the topology of T #) is set

K10( the carrier of TopStruct(# the carrier of T, the topology of T #)) is set

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

the topology of TopStruct(# the carrier of T, the topology of T #) is Element of K10(K10( the carrier of TopStruct(# the carrier of T, the topology of T #)))

K10(K10( the carrier of TopStruct(# the carrier of T, the topology of T #))) is set

X2 is Element of K10( the carrier of TopStruct(# the carrier of T, the topology of T #))

Y1 is Element of K10( the carrier of T)

Y2 is Element of K10( the carrier of T)

Y2 /\ ([#] TopStruct(# the carrier of T, the topology of T #)) is Element of K10( the carrier of TopStruct(# the carrier of T, the topology of T #))

Y1 is Element of K10( the carrier of T)

Y1 /\ ([#] TopStruct(# the carrier of T, the topology of T #)) is Element of K10( the carrier of TopStruct(# the carrier of T, the topology of T #))

T is TopSpace-like TopStruct

the carrier of T is set

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

K10( the carrier of T) is set

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

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

X1 is strict TopSpace-like SubSpace of T

X2 is Element of K10( the carrier of T)

the carrier of X1 is set

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

T is non empty TopSpace-like TopStruct

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

the carrier of T is non empty set

K10( the carrier of T) is set

T | ([#] T) is non empty strict TopSpace-like SubSpace of T

X1 is Element of K10( the carrier of T)

the carrier of (T | ([#] T)) is non empty set

[#] (T | ([#] T)) is non empty non proper open closed Element of K10( the carrier of (T | ([#] T)))

K10( the carrier of (T | ([#] T))) is set

T is TopSpace-like TopStruct

the carrier of T is set

K10( the carrier of T) is set

X1 is TopSpace-like SubSpace of T

the carrier of X1 is set

X2 is Element of K10( the carrier of T)

Y1 is Element of K10( the carrier of T)

T is TopSpace-like TopStruct

the carrier of T is set

K10( the carrier of T) is set

X1 is TopSpace-like (T) SubSpace of T

the carrier of X1 is set

K10( the carrier of X1) is set

X2 is Element of K10( the carrier of T)

Y1 is Element of K10( the carrier of X1)

Y2 is Element of K10( the carrier of T)

T is TopSpace-like TopStruct

X1 is TopSpace-like (T) SubSpace of T

X2 is TopSpace-like (X1) SubSpace of X1

the carrier of T is set

K10( the carrier of T) is set

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

the carrier of X1 is set

K10( the carrier of X1) is set

Y2 is Element of K10( the carrier of T)

the carrier of X2 is set

C2 is Element of K10( the carrier of X1)

Y1 is Element of K10( the carrier of T)

C1 is Element of K10( the carrier of T)

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

T is non empty TopSpace-like TopStruct

X1 is TopSpace-like (T) SubSpace of T

the carrier of X1 is set

X2 is non empty TopSpace-like SubSpace of T

the carrier of X2 is non empty set

K10( the carrier of X2) is set

Y2 is Element of K10( the carrier of X2)

the carrier of T is non empty set

K10( the carrier of T) is set

C2 is Element of K10( the carrier of T)

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

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

Y1 is Element of K10( the carrier of X2)

T is non empty TopSpace-like TopStruct

the carrier of T is non empty set

K10( the carrier of T) is set

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

X2 is non empty strict TopSpace-like SubSpace of T

the carrier of X2 is non empty set

Y1 is non empty strict TopSpace-like (T) SubSpace of T

the carrier of Y1 is non empty set

T is non empty TopStruct

X1 is non empty SubSpace of T

the carrier of X1 is non empty set

X2 is non empty SubSpace of T

the carrier of X2 is non empty set

the carrier of X1 \/ the carrier of X2 is non empty set

the carrier of T is non empty set

K10( the carrier of T) is set

Y1 is Element of K10( the carrier of T)

Y2 is Element of K10( the carrier of T)

Y1 \/ Y2 is Element of K10( the carrier of T)

C1 is non empty Element of K10( the carrier of T)

T | C1 is non empty strict SubSpace of T

the carrier of (T | C1) is non empty set

[#] (T | C1) is non empty non proper Element of K10( the carrier of (T | C1))

K10( the carrier of (T | C1)) is set

Y1 is non empty strict SubSpace of T

the carrier of Y1 is non empty set

Y2 is non empty strict SubSpace of T

the carrier of Y2 is non empty set

Y1 is non empty strict SubSpace of T

the carrier of Y1 is non empty set

Y2 is non empty SubSpace of T

the carrier of Y2 is non empty set

C2 is non empty SubSpace of T

the carrier of C2 is non empty set

the carrier of Y2 \/ the carrier of C2 is non empty set

the carrier of C2 \/ the carrier of Y2 is non empty set

T is non empty TopSpace-like TopStruct

X1 is non empty TopSpace-like SubSpace of T

X2 is non empty TopSpace-like SubSpace of T

(T,X1,X2) is non empty strict TopSpace-like SubSpace of T

Y1 is non empty TopSpace-like SubSpace of T

(T,(T,X1,X2),Y1) is non empty strict TopSpace-like SubSpace of T

(T,X2,Y1) is non empty strict TopSpace-like SubSpace of T

(T,X1,(T,X2,Y1)) is non empty strict TopSpace-like SubSpace of T

the carrier of (T,(T,X1,X2),Y1) is non empty set

the carrier of (T,X1,X2) is non empty set

the carrier of Y1 is non empty set

the carrier of (T,X1,X2) \/ the carrier of Y1 is non empty set

the carrier of X1 is non empty set

the carrier of X2 is non empty set

the carrier of X1 \/ the carrier of X2 is non empty set

( the carrier of X1 \/ the carrier of X2) \/ the carrier of Y1 is non empty set

the carrier of X2 \/ the carrier of Y1 is non empty set

the carrier of X1 \/ ( the carrier of X2 \/ the carrier of Y1) is non empty set

the carrier of (T,X2,Y1) is non empty set

the carrier of X1 \/ the carrier of (T,X2,Y1) is non empty set

the carrier of (T,X1,(T,X2,Y1)) is non empty set

T is non empty TopSpace-like TopStruct

X1 is non empty TopSpace-like SubSpace of T

X2 is non empty TopSpace-like SubSpace of T

(T,X1,X2) is non empty strict TopSpace-like SubSpace of T

the carrier of X1 is non empty set

the carrier of X2 is non empty set

the carrier of (T,X1,X2) is non empty set

the carrier of X1 \/ the carrier of X2 is non empty set

T is non empty TopSpace-like TopStruct

X1 is non empty TopSpace-like SubSpace of T

X2 is non empty TopSpace-like SubSpace of T

(T,X1,X2) is non empty strict TopSpace-like SubSpace of T

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 X1 is non empty set

the carrier of X1 \/ the carrier of X2 is non empty set

the carrier of TopStruct(# the carrier of X2, the topology of X2 #) is non empty set

the carrier of X1 \/ the carrier of X2 is non empty set

T is non empty TopSpace-like TopStruct

X1 is non empty TopSpace-like closed SubSpace of T

X2 is non empty TopSpace-like closed SubSpace of T

(T,X1,X2) is non empty strict TopSpace-like SubSpace of T

the carrier of T is non empty set

K10( the carrier of T) is set

the carrier of X2 is non empty set

the carrier of X1 is non empty set

the carrier of (T,X1,X2) is non empty set

Y2 is Element of K10( the carrier of T)

Y1 is Element of K10( the carrier of T)

Y2 \/ Y1 is Element of K10( the carrier of T)

C2 is Element of K10( the carrier of T)

T is non empty TopSpace-like TopStruct

X1 is non empty TopSpace-like (T) SubSpace of T

X2 is non empty TopSpace-like (T) SubSpace of T

(T,X1,X2) is non empty strict TopSpace-like SubSpace of T

the carrier of T is non empty set

K10( the carrier of T) is set

the carrier of X2 is non empty set

the carrier of X1 is non empty set

the carrier of (T,X1,X2) is non empty set

Y2 is Element of K10( the carrier of T)

Y1 is Element of K10( the carrier of T)

Y2 \/ Y1 is Element of K10( the carrier of T)

C2 is Element of K10( the carrier of T)

X2 is 1-sorted

the carrier of X2 is set

Y1 is 1-sorted

the carrier of Y1 is set

T is non empty TopStruct

X1 is non empty SubSpace of T

X2 is non empty SubSpace of T

the carrier of X1 is non empty set

the carrier of X2 is non empty set

the carrier of X1 /\ the carrier of X2 is set

the carrier of T is non empty set

K10( the carrier of T) is set

Y1 is Element of K10( the carrier of T)

Y2 is Element of K10( the carrier of T)

Y1 /\ Y2 is Element of K10( the carrier of T)

C1 is non empty Element of K10( the carrier of T)

T | C1 is non empty strict SubSpace of T

the carrier of (T | C1) is non empty set

[#] (T | C1) is non empty non proper Element of K10( the carrier of (T | C1))

K10( the carrier of (T | C1)) is set

Y1 is non empty strict SubSpace of T

the carrier of Y1 is non empty set

Y2 is non empty strict SubSpace of T

the carrier of Y2 is non empty set

T is non empty TopSpace-like TopStruct

X1 is non empty TopSpace-like SubSpace of T

X2 is non empty TopSpace-like SubSpace of T

(T,X1,X2) is non empty strict TopSpace-like SubSpace of T

(T,X2,X1) is non empty strict TopSpace-like SubSpace of T

Y1 is non empty TopSpace-like SubSpace of T

(T,X2,Y1) is non empty strict TopSpace-like SubSpace of T

(T,(T,X1,X2),Y1) is non empty strict TopSpace-like SubSpace of T

(T,X1,(T,X2,Y1)) is non empty strict TopSpace-like SubSpace of T

the carrier of (T,X1,X2) is non empty set

the carrier of X2 is non empty set

the carrier of X1 is non empty set

the carrier of X2 /\ the carrier of X1 is set

the carrier of (T,X2,X1) is non empty set

the carrier of (T,X1,X2) is non empty set

the carrier of Y1 is non empty set

the carrier of (T,X1,X2) /\ the carrier of Y1 is set

the carrier of X1 is non empty set

the carrier of X2 is non empty set

the carrier of X1 /\ the carrier of X2 is set

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

the carrier of X2 /\ the carrier of Y1 is set

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

the carrier of (T,X2,Y1) is non empty set

the carrier of X1 /\ the carrier of (T,X2,Y1) is set

the carrier of (T,(T,X1,X2),Y1) is non empty set

the carrier of (T,X1,(T,X2,Y1)) is non empty set

T is non empty TopSpace-like TopStruct

X1 is non empty TopSpace-like SubSpace of T

X2 is non empty TopSpace-like SubSpace of T

(T,X1,X2) is non empty strict TopSpace-like SubSpace of T

the carrier of (T,X1,X2) is non empty set

the carrier of X1 is non empty set

the carrier of X2 is non empty set

the carrier of X1 /\ the carrier of X2 is set

T is non empty TopSpace-like TopStruct

X1 is non empty TopSpace-like SubSpace of T

X2 is non empty TopSpace-like SubSpace of T

(T,X1,X2) is non empty strict TopSpace-like SubSpace of T

the carrier of X1 is non empty set

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

K10( the carrier of X1) is set

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

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

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 X1 /\ the carrier of X2 is set

the carrier of TopStruct(# the carrier of X1, the topology of X1 #) is non empty set

the carrier of X1 /\ the carrier of X2 is set

the carrier of X1 /\ the carrier of X2 is set

the carrier of TopStruct(# the carrier of X2, the topology of X2 #) is non empty set

the carrier of X1 /\ the carrier of X2 is set

T is non empty TopSpace-like TopStruct

X1 is non empty TopSpace-like closed SubSpace of T

X2 is non empty TopSpace-like closed SubSpace of T

(T,X1,X2) is non empty strict TopSpace-like SubSpace of T

the carrier of T is non empty set

K10( the carrier of T) is set

the carrier of X2 is non empty set

the carrier of X1 is non empty set

the carrier of (T,X1,X2) is non empty set

Y2 is Element of K10( the carrier of T)

Y1 is Element of K10( the carrier of T)

Y2 /\ Y1 is Element of K10( the carrier of T)

C2 is Element of K10( the carrier of T)

T is non empty TopSpace-like TopStruct

X1 is non empty TopSpace-like (T) SubSpace of T

X2 is non empty TopSpace-like (T) SubSpace of T

(T,X1,X2) is non empty strict TopSpace-like SubSpace of T

the carrier of T is non empty set

K10( the carrier of T) is set

the carrier of X2 is non empty set

the carrier of X1 is non empty set

the carrier of (T,X1,X2) is non empty set

Y2 is Element of K10( the carrier of T)

Y1 is Element of K10( the carrier of T)

Y2 /\ Y1 is Element of K10( the carrier of T)

C2 is Element of K10( the carrier of T)

T is non empty TopSpace-like TopStruct

X1 is non empty TopSpace-like SubSpace of T

X2 is non empty TopSpace-like SubSpace of T

(T,X1,X2) is non empty strict TopSpace-like SubSpace of T

(T,X1,X2) is non empty strict TopSpace-like SubSpace of T

T is non empty TopSpace-like TopStruct

X1 is non empty TopSpace-like SubSpace of T

X2 is non empty TopSpace-like SubSpace of T

(T,X1,X2) is non empty strict TopSpace-like SubSpace of T

Y1 is non empty TopSpace-like SubSpace of T

(T,(T,X1,X2),Y1) is non empty strict TopSpace-like SubSpace of T

(T,X1,Y1) is non empty strict TopSpace-like SubSpace of T

(T,X2,Y1) is non empty strict TopSpace-like SubSpace of T

(T,(T,X1,Y1),(T,X2,Y1)) is non empty strict TopSpace-like SubSpace of T

(T,Y1,(T,X1,X2)) is non empty strict TopSpace-like SubSpace of T

(T,Y1,X1) is non empty strict TopSpace-like SubSpace of T

(T,Y1,X2) is non empty strict TopSpace-like SubSpace of T

(T,(T,Y1,X1),(T,Y1,X2)) is non empty strict TopSpace-like SubSpace of T

the carrier of X1 is non empty set

the carrier of (T,X1,X2) is non empty set

the carrier of Y1 is non empty set

the carrier of X1 /\ the carrier of Y1 is set

the carrier of (T,X1,X2) /\ the carrier of Y1 is set

the carrier of (T,(T,X1,X2),Y1) is non empty set

the carrier of X2 is non empty set

the carrier of X1 \/ the carrier of X2 is non empty set

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

the carrier of X2 /\ the carrier of Y1 is set

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

the carrier of (T,X1,Y1) is non empty set

the carrier of (T,X1,Y1) \/ ( the carrier of X2 /\ the carrier of Y1) is non empty set

the carrier of (T,X2,Y1) is non empty set

the carrier of (T,X1,Y1) \/ the carrier of (T,X2,Y1) is non empty set

the carrier of (T,(T,X1,Y1),(T,X2,Y1)) is non empty set

(T,(T,Y1,X1),(T,X2,Y1)) is non empty strict TopSpace-like SubSpace of T

T is non empty TopSpace-like TopStruct

X1 is non empty TopSpace-like SubSpace of T

X2 is non empty TopSpace-like SubSpace of T

(T,X1,X2) is non empty strict TopSpace-like SubSpace of T

Y1 is non empty TopSpace-like SubSpace of T

(T,(T,X1,X2),Y1) is non empty strict TopSpace-like SubSpace of T

(T,X1,Y1) is non empty strict TopSpace-like SubSpace of T

(T,X2,Y1) is non empty strict TopSpace-like SubSpace of T

(T,(T,X1,Y1),(T,X2,Y1)) is non empty strict TopSpace-like SubSpace of T

(T,Y1,(T,X1,X2)) is non empty strict TopSpace-like SubSpace of T

(T,Y1,X1) is non empty strict TopSpace-like SubSpace of T

(T,Y1,X2) is non empty strict TopSpace-like SubSpace of T

(T,(T,Y1,X1),(T,Y1,X2)) is non empty strict TopSpace-like SubSpace of T

the carrier of Y1 is non empty set

the carrier of (T,X2,Y1) is non empty set

the carrier of (T,X1,Y1) is non empty set

the carrier of (T,X1,Y1) /\ the carrier of (T,X2,Y1) is set

the carrier of (T,(T,X1,X2),Y1) is non empty set

the carrier of (T,X1,X2) is non empty set

the carrier of (T,X1,X2) \/ the carrier of Y1 is non empty set

the carrier of X1 is non empty set

the carrier of X2 is non empty set

the carrier of X1 /\ the carrier of X2 is set

( the carrier of X1 /\ the carrier of X2) \/ the carrier of Y1 is non empty set

the carrier of X1 \/ the carrier of Y1 is non empty set

the carrier of X2 \/ the carrier of Y1 is non empty set

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

the carrier of (T,X1,Y1) /\ ( the carrier of X2 \/ the carrier of Y1) is set

the carrier of (T,(T,X1,Y1),(T,X2,Y1)) is non empty set

T is TopStruct

the carrier of T is set

K10( the carrier of T) is set

T is TopSpace-like TopStruct

the carrier of T is set

K10( the carrier of T) is set

X1 is Element of K10( the carrier of T)

X2 is Element of K10( the carrier of T)

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

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

T is TopSpace-like TopStruct

the carrier of T is set

K10( the carrier of T) is set

X1 is Element of K10( the carrier of T)

X2 is Element of K10( the carrier of T)

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

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

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

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

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

T is TopSpace-like TopStruct

the carrier of T is set

K10( the carrier of T) is set

X1 is Element of K10( the carrier of T)

X2 is Element of K10( the carrier of T)

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

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

the carrier of T \ X1 is set

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

the carrier of T \ (X1 `) is set

T is TopSpace-like TopStruct

the carrier of T is set

K10( the carrier of T) is set

X1 is Element of K10( the carrier of T)

X2 is Element of K10( the carrier of T)

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

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

T is TopSpace-like TopStruct

the carrier of T is set

K10( the carrier of T) is set

X1 is Element of K10( the carrier of T)

X2 is Element of K10( the carrier of T)

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

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

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

the carrier of T \ (Cl X1) is set

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

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

the carrier of T \ (Cl X2) is set

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

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

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

X2 \ (Cl X2) is Element of K10( the carrier of T)

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

(X1 \ (Cl X2)) \/ {} is set

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

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

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

X1 \ (Cl X1) is Element of K10( the carrier of T)

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

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

{} \/ (X2 \ (Cl X1)) is set

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

T is TopSpace-like TopStruct

the carrier of T is set

K10( the carrier of T) is set

X1 is Element of K10( the carrier of T)

X2 is Element of K10( the carrier of T)

Y1 is Element of K10( the carrier of T)

X1 /\ Y1 is Element of K10( the carrier of T)

X2 /\ Y1 is Element of K10( the carrier of T)

T is TopSpace-like TopStruct

the carrier of T is set

K10( the carrier of T) is set

X1 is Element of K10( the carrier of T)

X2 is Element of K10( the carrier of T)

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

Y1 is Element of K10( the carrier of T)

T is TopSpace-like TopStruct

the carrier of T is set

K10( the carrier of T) is set

X1 is Element of K10( the carrier of T)

X2 is Element of K10( the carrier of T)

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

Y1 is Element of K10( the carrier of T)

T is TopSpace-like TopStruct

the carrier of T is set

K10( the carrier of T) is set

X1 is Element of K10( the carrier of T)

X2 is Element of K10( the carrier of T)

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

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

Y1 is Element of K10( the carrier of T)

Y2 is Element of K10( the carrier of T)

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

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

T is TopSpace-like TopStruct

the carrier of T is set

K10( the carrier of T) is set

X1 is Element of K10( the carrier of T)

X2 is Element of K10( the carrier of T)

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

Y1 is Element of K10( the carrier of T)

Y2 is Element of K10( the carrier of T)

Y1 /\ Y2 is Element of K10( the carrier of T)

Y1 is Element of K10( the carrier of T)

Y2 is Element of K10( the carrier of T)

Y1 /\ Y2 is Element of K10( the carrier of T)

X1 /\ Y2 is Element of K10( the carrier of T)

(Y1 /\ Y2) /\ X1 is Element of K10( the carrier of T)

(Y1 /\ Y2) /\ (X1 \/ X2) is Element of K10( the carrier of T)

Y1 /\ X2 is Element of K10( the carrier of T)

(Y1 /\ Y2) /\ X2 is Element of K10( the carrier of T)

C2 is Element of K10( the carrier of T)

C1 is Element of K10( the carrier of T)

T is TopSpace-like TopStruct

the carrier of T is set

K10( the carrier of T) is set

X1 is Element of K10( the carrier of T)

X2 is Element of K10( the carrier of T)

Y1 is Element of K10( the carrier of T)

Y2 is Element of K10( the carrier of T)

Y2 ` is Element of K10( the carrier of T)

the carrier of T \ Y2 is set

Y1 ` is Element of K10( the carrier of T)

the carrier of T \ Y1 is set

Y1 is Element of K10( the carrier of T)

Y2 is Element of K10( the carrier of T)

Y2 ` is Element of K10( the carrier of T)

the carrier of T \ Y2 is set

Y1 ` is Element of K10( the carrier of T)

the carrier of T \ Y1 is set

C2 is Element of K10( the carrier of T)

C1 is Element of K10( the carrier of T)

T is TopSpace-like TopStruct

the carrier of T is set

K10( the carrier of T) is set

X1 is Element of K10( the carrier of T)

X2 is Element of K10( the carrier of T)

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

Y1 is Element of K10( the carrier of T)

Y2 is Element of K10( the carrier of T)

Y1 /\ Y2 is Element of K10( the carrier of T)

Y1 is Element of K10( the carrier of T)

Y2 is Element of K10( the carrier of T)

Y1 /\ Y2 is Element of K10( the carrier of T)

X1 /\ Y2 is Element of K10( the carrier of T)

(Y1 /\ Y2) /\ X1 is Element of K10( the carrier of T)

(Y1 /\ Y2) /\ (X1 \/ X2) is Element of K10( the carrier of T)

Y1 /\ X2 is Element of K10( the carrier of T)

(Y1 /\ Y2) /\ X2 is Element of K10( the carrier of T)

C2 is Element of K10( the carrier of T)

C1 is Element of K10( the carrier of T)

T is TopStruct

the carrier of T is set

K10( the carrier of T) is set

Y1 is Element of K10( the carrier of T)

Y2 is Element of K10( the carrier of T)

Y1 \ Y2 is Element of K10( the carrier of T)

Y2 \ Y1 is Element of K10( the carrier of T)

T is TopStruct

the carrier of T is set

K10( the carrier of T) is set

T is TopSpace-like TopStruct

the carrier of T is set

K10( the carrier of T) is set

X1 is Element of K10( the carrier of T)

X2 is Element of K10( the carrier of T)

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

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

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

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

T is TopSpace-like TopStruct

the carrier of T is set

K10( the carrier of T) is set

X1 is Element of K10( the carrier of T)

X2 is Element of K10( the carrier of T)

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

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

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

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

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

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

T is TopSpace-like TopStruct

the carrier of T is set

K10( the carrier of T) is set

X1 is Element of K10( the carrier of T)

X2 is Element of K10( the carrier of T)

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

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

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

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

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

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

T is TopSpace-like TopStruct

the carrier of T is set

K10( the carrier of T) is set

X1 is Element of K10( the carrier of T)

X2 is Element of K10( the carrier of T)

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

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

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

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

T is TopSpace-like TopStruct

the carrier of T is set

K10( the carrier of T) is set

X1 is Element of K10( the carrier of T)

X2 is Element of K10( the carrier of T)

Y1 is Element of K10( the carrier of T)

X1 \/ Y1 is Element of K10( the carrier of T)

X2 \/ Y1 is Element of K10( the carrier of T)

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

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

Y1 \ (X2 \/ Y1) is Element of K10( the carrier of T)

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

(X1 \ (X2 \/ Y1)) \/ {} is set

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

X1 \ Y1 is Element of K10( the carrier of T)

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

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

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

Y1 \ (X1 \/ Y1) is Element of K10( the carrier of T)

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

(X2 \ (X1 \/ Y1)) \/ {} is set

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

X2 \ Y1 is Element of K10( the carrier of T)

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

T is TopSpace-like TopStruct

the carrier of T is set

K10( the carrier of T) is set

X1 is Element of K10( the carrier of T)

X2 is Element of K10( the carrier of T)

Y1 is Element of K10( the carrier of T)

Y2 is Element of K10( the carrier of T)

X2 \/ Y1 is Element of K10( the carrier of T)

X1 \/ Y2 is Element of K10( the carrier of T)

Y1 \ (X1 \/ Y2) is Element of K10( the carrier of T)

Y2 \ (X2 \/ Y1) is Element of K10( the carrier of T)

(X1 \/ Y2) \ (X2 \/ Y1) is Element of K10( the carrier of T)

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

(X1 \ (X2 \/ Y1)) \/ (Y2 \ (X2 \/ Y1)) is Element of K10( the carrier of T)

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

(X2 \/ Y1) \ (X1 \/ Y2) is Element of K10( the carrier of T)

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

(X2 \ (X1 \/ Y2)) \/ (Y1 \ (X1 \/ Y2)) is Element of K10( the carrier of T)

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

T is TopSpace-like TopStruct

the carrier of T is set

K10( the carrier of T) is set

X1 is Element of K10( the carrier of T)

X2 is Element of K10( the carrier of T)

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

Y1 is Element of K10( the carrier of T)

X2 \ Y1 is Element of K10( the carrier of T)

Y1 \ X2 is Element of K10( the carrier of T)

X1 \ Y1 is Element of K10( the carrier of T)

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

Y1 \ X1 is Element of K10( the carrier of T)

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

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

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

T is TopSpace-like TopStruct

the carrier of T is set

K10( the carrier of T) is set

X1 is Element of K10( the carrier of T)

X2 is Element of K10( the carrier of T)

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

Y1 is Element of K10( the carrier of T)

X2 \ Y1 is Element of K10( the carrier of T)

Y1 \ X2 is Element of K10( the carrier of T)

Y1 \ X1 is Element of K10( the carrier of T)

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

X1 \ Y1 is Element of K10( the carrier of T)

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

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

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

T is TopSpace-like TopStruct

the carrier of T is set

K10( the carrier of T) is set

X1 is Element of K10( the carrier of T)

X2 is Element of K10( the carrier of T)

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

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

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

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

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

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

C2 is Element of K10( the carrier of T)

C1 is Element of K10( the carrier of T)

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

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

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

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

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

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

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

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

the carrier of T \ (C2 \/ C1) is set

A1 is Element of K10( the carrier of T)

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

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

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

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

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

X1 \+\ X2 is Element of K10( the carrier of T)

(X1 \+\ X2) ` is Element of K10( the carrier of T)

the carrier of T \ (X1 \+\ X2) is set

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

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

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

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

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

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

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

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

{} T is empty open closed Element of K10( the carrier of T)

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

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

C1 /\ X1 is Element of K10( the carrier of T)

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

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

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

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

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

A1 ` is Element of K10( the carrier of T)

the carrier of T \ A1 is set

A1 \/ (A1 `) is Element of K10( the carrier of T)

C2 is Element of K10( the carrier of T)

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

C1 is Element of K10( the carrier of T)

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

A1 is Element of K10( the carrier of T)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

(C1 /\ (X1 \/ X2)) \/ (A1 /\ (X1 \/ X2)) is Element of K10( the carrier of T)

C1 \/ A1 is Element of K10( the carrier of T)

(C1 \/ A1) /\ (X1 \/ X2) is Element of K10( the carrier of T)

(X1 \/ X2) \ ((C1 \/ A1) /\ (X1 \/ X2)) is Element of K10( the carrier of T)

(X1 \/ X2) \ (C1 \/ A1) is Element of K10( the carrier of T)

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

A1 \/ C2 is Element of K10( the carrier of T)

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

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

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

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

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

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

A2 is Element of K10( the carrier of T)

c

A2 /\ c

T is non empty TopSpace-like TopStruct

the carrier of T is non empty set

K10( the carrier of T) is set

X1 is Element of K10( the carrier of T)

X2 is Element of K10( the carrier of T)

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

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

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

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

C2 is Element of K10( the carrier of T)

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

C1 is Element of K10( the carrier of T)

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

A1 is Element of K10( the carrier of T)

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

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

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

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

A1 \/ C2 is Element of K10( the carrier of T)

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

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

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

(C1 /\ (X1 \/ X2)) \/ (A1 /\ (X1 \/ X2)) is Element of K10( the carrier of T)

C1 \/ A1 is Element of K10( the carrier of T)

(C1 \/ A1) /\ (X1 \/ X2) is Element of K10( the carrier of T)

(X1 \/ X2) \ ((C1 \/ A1) /\ (X1 \/ X2)) is Element of K10( the carrier of T)

(X1 \/ X2) \ (C1 \/ A1) is Element of K10( the carrier of T)

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

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

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

c

c

A2 is non empty Element of K10( the carrier of T)

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

c

Y is non empty Element of K10( the carrier of T)

(C2 \/ C1) \/ Y is non empty Element of K10( the carrier of T)

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

Y is non empty Element of K10( the carrier of T)

(C2 \/ C1) \/ Y is non empty Element of K10( the carrier of T)

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

T is non empty TopSpace-like TopStruct

the carrier of T is non empty set

K10( the carrier of T) is set

X1 is Element of K10( the carrier of T)

X2 is Element of K10( the carrier of T)

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

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

Y1 is Element of K10( the carrier of T)

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

Y2 is Element of K10( the carrier of T)

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

C2 is Element of K10( the carrier of T)

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

Y1 \/ Y2 is Element of K10( the carrier of T)

(Y1 \/ Y2) \/ C2 is Element of K10( the carrier of T)

Y1 is Element of K10( the carrier of T)

Y2 is Element of K10( the carrier of T)

Y1 \/ Y2 is Element of K10( the carrier of T)

C2 is Element of K10( the carrier of T)

(Y1 \/ Y2) \/ C2 is Element of K10( the carrier of T)

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

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

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

C1 is Element of K10( the carrier of T)

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

A1 is Element of K10( the carrier of T)

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

A2 is Element of K10( the carrier of T)

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

C1 \/ A1 is Element of K10( the carrier of T)

(C1 \/ A1) \/ A2 is Element of K10( the carrier of T)

T is non empty TopSpace-like TopStruct

the carrier of T is non empty set

K10( the carrier of T) is set

X1 is Element of K10( the carrier of T)

X2 is Element of K10( the carrier of T)

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

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

Y1 is non empty Element of K10( the carrier of T)

Y2 is non empty Element of K10( the carrier of T)

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

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

Y1 \/ Y2 is non empty Element of K10( the carrier of T)

C2 is non empty Element of K10( the carrier of T)

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

(Y1 \/ Y2) \/ C2 is non empty Element of K10( the carrier of T)

C2 is non empty Element of K10( the carrier of T)

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

(Y1 \/ Y2) \/ C2 is non empty Element of K10( the carrier of T)

C2 is non empty Element of K10( the carrier of T)

(Y1 \/ Y2) \/ C2 is non empty Element of K10( the carrier of T)

T is non empty TopSpace-like TopStruct

the carrier of T is non empty set

K10( the carrier of T) is set

X1 is Element of K10( the carrier of T)

X2 is Element of K10( the carrier of T)

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

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

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

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

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

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

C2 is Element of K10( the carrier of T)

C1 is Element of K10( the carrier of T)

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

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

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

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

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

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

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

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

the carrier of T \ (C2 \/ C1) is set

A1 is Element of K10( the carrier of T)

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

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

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

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

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

X1 \+\ X2 is Element of K10( the carrier of T)

(X1 \+\ X2) ` is Element of K10( the carrier of T)

the carrier of T \ (X1 \+\ X2) is set

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

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

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

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

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

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

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

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

{} T is empty open closed Element of K10( the carrier of T)

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

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

C1 /\ X1 is Element of K10( the carrier of T)

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

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

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

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

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

A1 ` is Element of K10( the carrier of T)

the carrier of T \ A1 is set

(A1 `) \/ A1 is Element of K10( the carrier of T)

C2 is Element of K10( the carrier of T)

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

C1 is Element of K10( the carrier of T)

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

A1 is Element of K10( the carrier of T)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

(C1 /\ (X1 \/ X2)) \/ (A1 /\ (X1 \/ X2)) is Element of K10( the carrier of T)

C1 \/ A1 is Element of K10( the carrier of T)

(C1 \/ A1) /\ (X1 \/ X2) is Element of K10( the carrier of T)

(X1 \/ X2) \ ((C1 \/ A1) /\ (X1 \/ X2)) is Element of K10( the carrier of T)

(X1 \/ X2) \ (C1 \/ A1) is Element of K10( the carrier of T)

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

A1 \/ C2 is Element of K10( the carrier of T)

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

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

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

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

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

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

A2 is Element of K10( the carrier of T)

c

A2 /\ c

T is non empty TopSpace-like TopStruct

the carrier of T is non empty set

K10( the carrier of T) is set

X1 is Element of K10( the carrier of T)

X2 is Element of K10( the carrier of T)

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

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

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

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

C2 is Element of K10( the carrier of T)

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

C1 is Element of K10( the carrier of T)

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

A1 is Element of K10( the carrier of T)

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

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

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

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

A1 \/ C2 is Element of K10( the carrier of T)

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

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

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

(C1 /\ (X1 \/ X2)) \/ (A1 /\ (X1 \/ X2)) is Element of K10( the carrier of T)

C1 \/ A1 is Element of K10( the carrier of T)

(C1 \/ A1) /\ (X1 \/ X2) is Element of K10( the carrier of T)

(X1 \/ X2) \ ((C1 \/ A1) /\ (X1 \/ X2)) is Element of K10( the carrier of T)

(X1 \/ X2) \ (C1 \/ A1) is Element of K10( the carrier of T)

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

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

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

c

c

A2 is non empty Element of K10( the carrier of T)

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

c

Y is non empty Element of K10( the carrier of T)

(C2 \/ C1) \/ Y is non empty Element of K10( the carrier of T)

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

Y is non empty Element of K10( the carrier of T)

(C2 \/ C1) \/ Y is non empty Element of K10( the carrier of T)

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

T is non empty TopSpace-like TopStruct

the carrier of T is non empty set

K10( the carrier of T) is set

X1 is Element of K10( the carrier of T)

X2 is Element of K10( the carrier of T)

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

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

Y1 is Element of K10( the carrier of T)

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

Y2 is Element of K10( the carrier of T)

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

C2 is Element of K10( the carrier of T)

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

Y1 \/ Y2 is Element of K10( the carrier of T)

(Y1 \/ Y2) \/ C2 is Element of K10( the carrier of T)

Y1 is Element of K10( the carrier of T)

Y2 is Element of K10( the carrier of T)

Y1 \/ Y2 is Element of K10( the carrier of T)

C2 is Element of K10( the carrier of T)

(Y1 \/ Y2) \/ C2 is Element of K10( the carrier of T)

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

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

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

C1 is Element of K10( the carrier of T)

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

A1 is Element of K10( the carrier of T)

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

A2 is Element of K10( the carrier of T)

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

C1 \/ A1 is Element of K10( the carrier of T)

(C1 \/ A1) \/ A2 is Element of K10( the carrier of T)

T is non empty TopSpace-like TopStruct

the carrier of T is non empty set

K10( the carrier of T) is set

X1 is Element of K10( the carrier of T)

X2 is Element of K10( the carrier of T)

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

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

Y1 is non empty Element of K10( the carrier of T)

Y2 is non empty Element of K10( the carrier of T)

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

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

Y1 \/ Y2 is non empty Element of K10( the carrier of T)

C2 is non empty Element of K10( the carrier of T)

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

(Y1 \/ Y2) \/ C2 is non empty Element of K10( the carrier of T)

C2 is non empty Element of K10( the carrier of T)

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

(Y1 \/ Y2) \/ C2 is non empty Element of K10( the carrier of T)

C2 is non empty Element of K10( the carrier of T)

(Y1 \/ Y2) \/ C2 is non empty Element of K10( the carrier of T)

T is non empty TopSpace-like TopStruct

the carrier of T is non empty set

K10( the carrier of T) is set

X1 is Element of K10( the carrier of T)

X2 is Element of K10( the carrier of T)

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

Y1 is Element of K10( the carrier of T)

Y2 is Element of K10( the carrier of T)

Y1 /\ Y2 is Element of K10( the carrier of T)

Y1 is Element of K10( the carrier of T)

Y2 is Element of K10( the carrier of T)

Y1 /\ Y2 is Element of K10( the carrier of T)

(Y1 /\ Y2) /\ X1 is Element of K10( the carrier of T)

(Y1 /\ Y2) /\ X2 is Element of K10( the carrier of T)

Y1 /\ X2 is Element of K10( the carrier of T)

X2 \ Y1 is Element of K10( the carrier of T)

Y2 \ Y1 is Element of K10( the carrier of T)

X2 \ (Y1 /\ X2) is Element of K10( the carrier of T)

X1 /\ Y2 is Element of K10( the carrier of T)

X1 \ Y2 is Element of K10( the carrier of T)

Y1 \ Y2 is Element of K10( the carrier of T)

X1 \ (X1 /\ Y2) is Element of K10( the carrier of T)

T is TopStruct

the carrier of T is set

K10( the carrier of T) is set

Y1 is SubSpace of T

the carrier of Y1 is set

Y2 is SubSpace of T

the carrier of Y2 is set

C2 is Element of K10( the carrier of T)

C1 is Element of K10( the carrier of T)

T is TopStruct

T is non empty TopSpace-like TopStruct

X1 is non empty TopSpace-like SubSpace of T

X2 is non empty TopSpace-like SubSpace of T

the carrier of T is non empty set

K10( the carrier of T) is set

the carrier of X2 is non empty set

the carrier of X1 is non empty set

Y2 is Element of K10( the carrier of T)

Y1 is Element of K10( the carrier of T)

T is non empty TopSpace-like TopStruct

X1 is non empty TopSpace-like closed SubSpace of T

X2 is non empty TopSpace-like closed SubSpace of T

the carrier of T is non empty set

K10( the carrier of T) is set

the carrier of X2 is non empty set

the carrier of X1 is non empty set

Y2 is Element of K10( the carrier of T)

Y1 is Element of K10( the carrier of T)

C2 is Element of K10( the carrier of T)

C1 is Element of K10( the carrier of T)

T is non empty TopSpace-like TopStruct

X1 is non empty TopSpace-like SubSpace of T

X2 is non empty TopSpace-like SubSpace of T

(T,X1,X2) is non empty strict TopSpace-like SubSpace of T

the carrier of T is non empty set

K10( the carrier of T) is set

the carrier of X2 is non empty set

the carrier of X1 is non empty set

Y2 is Element of K10( the carrier of T)

Y1 is Element of K10( the carrier of T)

Y2 \/ Y1 is Element of K10( the carrier of T)

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

T is non empty TopSpace-like TopStruct

X1 is non empty TopSpace-like SubSpace of T

X2 is non empty TopSpace-like SubSpace of T

(T,X1,X2) is non empty strict TopSpace-like SubSpace of T

the carrier of T is non empty set

K10( the carrier of T) is set

the carrier of X2 is non empty set

the carrier of X1 is non empty set

Y2 is Element of K10( the carrier of T)

Y1 is Element of K10( the carrier of T)

Y2 \/ Y1 is Element of K10( the carrier of T)

the carrier of (T,X1,X2) is non empty set

T is non empty TopSpace-like TopStruct

X1 is non empty TopSpace-like (T) SubSpace of T

X2 is non empty TopSpace-like (T) SubSpace of T

the carrier of T is non empty set

K10( the carrier of T) is set

the carrier of X2 is non empty set

the carrier of X1 is non empty set

Y2 is Element of K10( the carrier of T)

Y1 is Element of K10( the carrier of T)

C2 is Element of K10( the carrier of T)

C1 is Element of K10( the carrier of T)

T is non empty TopSpace-like TopStruct

X1 is non empty TopSpace-like SubSpace of T

X2 is non empty TopSpace-like SubSpace of T

(T,X1,X2) is non empty strict TopSpace-like SubSpace of T

the carrier of T is non empty set

K10( the carrier of T) is set

the carrier of X2 is non empty set

the carrier of X1 is non empty set

Y2 is Element of K10( the carrier of T)

Y1 is Element of K10( the carrier of T)

Y2 \/ Y1 is Element of K10( the carrier of T)

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

T is non empty TopSpace-like TopStruct

X1 is non empty TopSpace-like SubSpace of T

X2 is non empty TopSpace-like SubSpace of T

(T,X1,X2) is non empty strict TopSpace-like SubSpace of T

the carrier of T is non empty set

K10( the carrier of T) is set

the carrier of X2 is non empty set

the carrier of X1 is non empty set

Y2 is Element of K10( the carrier of T)

Y1 is Element of K10( the carrier of T)

Y2 \/ Y1 is Element of K10( the carrier of T)

the carrier of (T,X1,X2) is non empty set

T is non empty TopSpace-like TopStruct

X2 is non empty TopSpace-like SubSpace of T

X1 is non empty TopSpace-like SubSpace of T

Y1 is non empty TopSpace-like SubSpace of T

(T,X2,X1) is non empty strict TopSpace-like SubSpace of T

(T,Y1,X1) is non empty strict TopSpace-like SubSpace of T

(T,X1,X2) is non empty strict TopSpace-like SubSpace of T

(T,X1,Y1) is non empty strict TopSpace-like SubSpace of T

the carrier of T is non empty set

K10( the carrier of T) is set

the carrier of Y1 is non empty set

the carrier of X2 is non empty set

the carrier of X1 is non empty set

C2 is Element of K10( the carrier of T)

Y2 is Element of K10( the carrier of T)

A1 is Element of K10( the carrier of T)

the carrier of (T,X2,X1) is non empty set

A2 is Element of K10( the carrier of T)

the carrier of (T,Y1,X1) is non empty set

C1 is Element of K10( the carrier of T)

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

Y2 /\ C1 is Element of K10( the carrier of T)

T is non empty TopSpace-like TopStruct

X1 is non empty TopSpace-like SubSpace of T

X2 is non empty TopSpace-like SubSpace of T

the carrier of T is non empty set

K10( the carrier of T) is set

the carrier of X2 is non empty set

the carrier of X1 is non empty set

C2 is TopSpace-like SubSpace of T

C1 is TopSpace-like SubSpace of T

A1 is Element of K10( the carrier of T)

the carrier of C2 is set

A2 is Element of K10( the carrier of T)

the carrier of C1 is set

Y2 is Element of K10( the carrier of T)

Y1 is Element of K10( the carrier of T)

T is non empty TopSpace-like TopStruct

X1 is non empty TopSpace-like SubSpace of T

X2 is non empty TopSpace-like SubSpace of T

(T,X1,X2) is non empty strict TopSpace-like SubSpace of T

Y1 is non empty TopSpace-like SubSpace of T

T is non empty TopSpace-like TopStruct

X1 is non empty TopSpace-like SubSpace of T

X2 is non empty TopSpace-like SubSpace of T

(T,X1,X2) is non empty strict TopSpace-like SubSpace of T

the carrier of T is non empty set

K10( the carrier of T) is set

the carrier of X2 is non empty set

the carrier of X1 is non empty set

C2 is non empty TopSpace-like SubSpace of T

the carrier of C2 is non empty set

Y2 is Element of K10( the carrier of T)

C1 is Element of K10( the carrier of T)

Y1 is Element of K10( the carrier of T)

A1 is Element of K10( the carrier of T)

the carrier of (T,X1,X2) is non empty set

A2 is Element of K10( the carrier of T)

Y2 \/ Y1 is Element of K10( the carrier of T)

T is non empty TopSpace-like TopStruct

X1 is non empty TopSpace-like SubSpace of T

X2 is non empty TopSpace-like SubSpace of T

the carrier of T is non empty set

K10( the carrier of T) is set

the carrier of X2 is non empty set

the carrier of X1 is non empty set

Y2 is Element of K10( the carrier of T)

Y1 is Element of K10( the carrier of T)

C2 is Element of K10( the carrier of T)

C1 is Element of K10( the carrier of T)

A1 is non empty strict TopSpace-like closed SubSpace of T

the carrier of A1 is non empty set

A2 is non empty strict TopSpace-like closed SubSpace of T

the carrier of A2 is non empty set

C2 is non empty TopSpace-like closed SubSpace of T

C1 is non empty TopSpace-like closed SubSpace of T

A1 is Element of K10( the carrier of T)

A2 is Element of K10( the carrier of T)

the carrier of C1 is non empty set

the carrier of C2 is non empty set

Y is Element of K10( the carrier of T)

c

c

Y is Element of K10( the carrier of T)

T is non empty TopSpace-like TopStruct

X1 is non empty TopSpace-like SubSpace of T

X2 is non empty TopSpace-like SubSpace of T

(T,X1,X2) is non empty strict TopSpace-like SubSpace of T

the carrier of T is non empty set

K10( the carrier of T) is set

the carrier of X2 is non empty set

the carrier of X1 is non empty set

Y2 is Element of K10( the carrier of T)

Y1 is Element of K10( the carrier of T)

Y2 \/ Y1 is Element of K10( the carrier of T)

C2 is Element of K10( the carrier of T)

C1 is Element of K10( the carrier of T)

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

A1 is non empty strict TopSpace-like closed SubSpace of T

the carrier of A1 is non empty set

A2 is non empty strict TopSpace-like closed SubSpace of T

the carrier of A2 is non empty set

(T,A1,A2) is non empty strict TopSpace-like SubSpace of T

the carrier of (T,A1,A2) is non empty set

the carrier of (T,X1,X2) is non empty set

C2 is non empty TopSpace-like closed SubSpace of T

C1 is non empty TopSpace-like closed SubSpace of T

(T,C2,C1) is non empty strict TopSpace-like SubSpace of T

A1 is Element of K10( the carrier of T)

A2 is Element of K10( the carrier of T)

A1 \/ A2 is Element of K10( the carrier of T)

the carrier of C1 is non empty set

the carrier of C2 is non empty set

Y is Element of K10( the carrier of T)

c

Y /\ c

the carrier of (T,X1,X2) is non empty set

the carrier of (T,C2,C1) is non empty set

c

Y is Element of K10( the carrier of T)

c

T is non empty TopSpace-like TopStruct

X1 is non empty TopSpace-like SubSpace of T

X2 is non empty TopSpace-like SubSpace of T

the carrier of T is non empty set

K10( the carrier of T) is set

the carrier of X2 is non empty set

the carrier of X1 is non empty set

Y2 is Element of K10( the carrier of T)

Y1 is Element of K10( the carrier of T)

C2 is Element of K10( the carrier of T)

C1 is Element of K10( the carrier of T)

A1 is non empty strict TopSpace-like (T) SubSpace of T

the carrier of A1 is non empty set

A2 is non empty strict TopSpace-like (T) SubSpace of T

the carrier of A2 is non empty set

C2 is non empty TopSpace-like (T) SubSpace of T

C1 is non empty TopSpace-like (T) SubSpace of T

A1 is Element of K10( the carrier of T)

A2 is Element of K10( the carrier of T)

the carrier of C1 is non empty set

the carrier of C2 is non empty set

Y is Element of K10( the carrier of T)

c

c

Y is Element of K10( the carrier of T)

T is non empty TopSpace-like TopStruct

X1 is non empty TopSpace-like SubSpace of T

X2 is non empty TopSpace-like SubSpace of T

(T,X1,X2) is non empty strict TopSpace-like SubSpace of T

the carrier of T is non empty set

K10( the carrier of T) is set

the carrier of X2 is non empty set

the carrier of X1 is non empty set

Y2 is Element of K10( the carrier of T)

Y1 is Element of K10( the carrier of T)

Y2 \/ Y1 is Element of K10( the carrier of T)

C2 is Element of K10( the carrier of T)

C1 is Element of K10( the carrier of T)

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

A1 is non empty strict TopSpace-like (T) SubSpace of T

the carrier of A1 is non empty set

A2 is non empty strict TopSpace-like (T) SubSpace of T

the carrier of A2 is non empty set

(T,A1,A2) is non empty strict TopSpace-like SubSpace of T

the carrier of (T,A1,A2) is non empty set

the carrier of (T,X1,X2) is non empty set

C2 is non empty TopSpace-like (T) SubSpace of T

C1 is non empty TopSpace-like (T) SubSpace of T

(T,C2,C1) is non empty strict TopSpace-like SubSpace of T

A1 is Element of K10( the carrier of T)

A2 is Element of K10( the carrier of T)

A1 \/ A2 is Element of K10( the carrier of T)

the carrier of C1 is non empty set

the carrier of C2 is non empty set

Y is Element of K10( the carrier of T)

c

Y /\ c

the carrier of (T,X1,X2) is non empty set

the carrier of (T,C2,C1) is non empty set

c

Y is Element of K10( the carrier of T)

c

T is TopStruct

the carrier of T is set

K10( the carrier of T) is set

Y1 is SubSpace of T

the carrier of Y1 is set

Y2 is SubSpace of T

the carrier of Y2 is set

C2 is Element of K10( the carrier of T)

C1 is Element of K10( the carrier of T)

T is TopStruct

T is non empty TopSpace-like TopStruct

X1 is non empty TopSpace-like SubSpace of T

X2 is non empty TopSpace-like SubSpace of T

the carrier of T is non empty set

K10( the carrier of T) is set

the carrier of X2 is non empty set

the carrier of X1 is non empty set

Y2 is Element of K10( the carrier of T)

Y1 is Element of K10( the carrier of T)

C2 is Element of K10( the carrier of T)

C1 is Element of K10( the carrier of T)

Y2 is Element of K10( the carrier of T)

Y1 is Element of K10( the carrier of T)

C2 is Element of K10( the carrier of T)

C1 is Element of K10( the carrier of T)

T is non empty TopSpace-like TopStruct

X1 is non empty TopSpace-like SubSpace of T

X2 is non empty TopSpace-like SubSpace of T

the carrier of T is non empty set

K10( the carrier of T) is set

Y1 is Element of K10( the carrier of T)

the carrier of X1 is non empty set

Y2 is