:: 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<sub>10</sub> is Element of K10( the carrier of T)
A2 /\ c<sub>10</sub> 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)
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<sub>10</sub> is non empty Element of K10( the carrier of T)
c<sub>10</sub> /\ (X1 \/ X2) is Element of K10( the carrier of T)
A2 is non empty Element of K10( the carrier of T)
A2 /\ (X1 \/ X2) is Element of K10( the carrier of T)
c<sub>10</sub> \/ A2 is non empty 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)
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₁₀ is Element of K10( the carrier of T)
A2 /\ c₁₀ 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)
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₁₀ is non empty Element of K10( the carrier of T)
c₁₀ /\ (X1 \/ X2) is Element of K10( the carrier of T)
A2 is non empty Element of K10( the carrier of T)
A2 /\ (X1 \/ X2) is Element of K10( the carrier of T)
c₁₀ \/ A2 is non empty 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)
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₁₀ is Element of K10( the carrier of T)
c₁₀ is Element of K10( the carrier of T)
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₁₀ is Element of K10( the carrier of T)
Y /\ c₁₀ is Element of K10( the carrier of T)
the carrier of (T,X1,X2) is non empty set
the carrier of (T,C2,C1) is non empty set
c₁₀ is Element of K10( the carrier of T)
Y is Element of K10( the carrier of T)
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
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₁₀ is Element of K10( the carrier of T)
c₁₀ is Element of K10( the carrier of T)
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₁₀ is Element of K10( the carrier of T)
Y /\ c₁₀ is Element of K10( the carrier of T)
the carrier of (T,X1,X2) is non empty set
the carrier of (T,C2,C1) is non empty set
c₁₀ is Element of K10( the carrier of T)
Y is Element of K10( the carrier of T)
c₁₀ /\ Y 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)
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 Element of K10( the carrier of T)
the carrier of X2 is non empty set
T is non empty TopSpace-like TopStruct
X1 is TopSpace-like closed SubSpace of T
X2 is TopSpace-like closed 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)
Y2 is Element of K10( the carrier of T)
the carrier of X1 is set
the carrier of X2 is set
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 TopSpace-like (T) SubSpace of T
X2 is TopSpace-like (T) 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)
Y2 is Element of K10( the carrier of T)
the carrier of X1 is set
the carrier of X2 is set
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
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
(T,X1,C2) is non empty strict TopSpace-like SubSpace of T
(T,X2,C2) is non empty strict TopSpace-like SubSpace of T
the carrier of C2 is non empty set
Y2 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,C2) is non empty set
A2 is Element of K10( the carrier of T)
the carrier of (T,X2,C2) is non empty set
C1 is Element of K10( the carrier of T)
Y2 \/ C1 is Element of K10( the carrier of T)
Y1 \/ 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 X1 is non empty set
the carrier of X2 is non empty set
C2 is non empty TopSpace-like SubSpace of T
C1 is non empty TopSpace-like SubSpace of T
(T,X2,C2) is non empty strict TopSpace-like SubSpace of T
(T,X1,C1) is non empty strict TopSpace-like SubSpace of T
(T,C2,X2) is non empty strict TopSpace-like SubSpace of T
(T,C1,X1) is non empty strict TopSpace-like SubSpace of T
the carrier of C1 is non empty set
the carrier of C2 is non empty set
Y2 is Element of K10( the carrier of T)
Y1 is Element of K10( the carrier of T)
A2 is Element of K10( the carrier of T)
A1 is Element of K10( the carrier of T)
c₁₀ is Element of K10( the carrier of T)
the carrier of (T,X2,C2) is non empty set
Y is Element of K10( the carrier of T)
the carrier of (T,X1,C1) is non empty set
Y2 \/ A2 is Element of K10( the carrier of T)
Y1 \/ A1 is Element of K10( the carrier of T)
T is non empty TopSpace-like TopStruct
X2 is non empty TopSpace-like SubSpace of T
Y1 is non empty TopSpace-like SubSpace of T
X1 is non empty TopSpace-like SubSpace of T
(T,X2,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)
C1 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,Y1) is non empty set
A2 is Element of K10( the carrier of T)
C2 /\ Y2 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
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
the carrier of T is non empty 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 non empty strict 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
the carrier of X2 is non empty set
the carrier of X1 is non empty set
[#] T is non empty non proper open closed Element of K10( the carrier of T)
C2 is non empty TopSpace-like closed SubSpace of T
(T,C2,(T,X1,X2)) is non empty strict TopSpace-like SubSpace of T
C1 is non empty TopSpace-like closed SubSpace of T
(T,C1,(T,X1,X2)) is non empty strict TopSpace-like SubSpace of T
(T,C2,C1) is non empty strict TopSpace-like SubSpace of T
A1 is non empty TopSpace-like (T) SubSpace of T
(T,(T,C2,C1),A1) is non empty strict TopSpace-like SubSpace of T
(T,A1,(T,X1,X2)) is non empty strict TopSpace-like SubSpace of T
C2 is non empty TopSpace-like closed SubSpace of T
(T,C2,(T,X1,X2)) is non empty strict TopSpace-like SubSpace of T
C1 is non empty TopSpace-like closed SubSpace of T
(T,C1,(T,X1,X2)) is non empty strict TopSpace-like SubSpace of T
(T,C2,C1) is non empty strict TopSpace-like SubSpace of T
the carrier of C1 is non empty set
the carrier of C2 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)
the carrier of (T,C2,C1) is non empty set
A2 is Element of K10( the carrier of T)
A1 is Element of K10( the carrier of T)
A2 \/ A1 is Element of K10( the carrier of T)
(A2 \/ A1) /\ (Y2 \/ Y1) is Element of K10( the carrier of T)
A2 /\ (Y2 \/ Y1) is Element of K10( the carrier of T)
A1 /\ (Y2 \/ Y1) is Element of K10( the carrier of T)
(A2 /\ (Y2 \/ Y1)) \/ (A1 /\ (Y2 \/ Y1)) is Element of K10( the carrier of T)
{} \/ (A1 /\ (Y2 \/ Y1)) is set
the carrier of (T,C1,(T,X1,X2)) is non empty set
c₁₀ is non empty TopSpace-like (T) SubSpace of T
(T,(T,C2,C1),c₁₀) is non empty strict TopSpace-like SubSpace of T
(T,c₁₀,(T,X1,X2)) is non empty strict TopSpace-like SubSpace of T
c₁₀ is non empty TopSpace-like (T) SubSpace of T
(T,(T,C2,C1),c₁₀) is non empty strict TopSpace-like SubSpace of T
(T,c₁₀,(T,X1,X2)) is non empty strict TopSpace-like SubSpace of T
the carrier of c₁₀ is non empty set
Y is Element of K10( the carrier of T)
(A2 \/ A1) \/ Y is Element of K10( the carrier of T)
((A2 \/ A1) \/ Y) /\ (Y2 \/ Y1) is Element of K10( the carrier of T)
A1 \/ Y is Element of K10( the carrier of T)
A2 \/ (A1 \/ Y) is Element of K10( the carrier of T)
(A2 \/ (A1 \/ Y)) /\ (Y2 \/ Y1) is Element of K10( the carrier of T)
A2 /\ (Y2 \/ Y1) is Element of K10( the carrier of T)
(A1 \/ Y) /\ (Y2 \/ Y1) is Element of K10( the carrier of T)
(A2 /\ (Y2 \/ Y1)) \/ ((A1 \/ Y) /\ (Y2 \/ Y1)) is Element of K10( the carrier of T)
{} \/ ((A1 \/ Y) /\ (Y2 \/ Y1)) is set
A1 /\ (Y2 \/ Y1) is Element of K10( the carrier of T)
Y /\ (Y2 \/ Y1) is Element of K10( the carrier of T)
(A1 /\ (Y2 \/ Y1)) \/ (Y /\ (Y2 \/ Y1)) is Element of K10( the carrier of T)
the carrier of (T,c₁₀,(T,X1,X2)) is non empty set
the carrier of (T,X1,X2) is non empty set
Y2 /\ Y1 is Element of K10( the carrier of T)
the carrier of (T,C1,(T,X1,X2)) is non empty set
the carrier of (T,C1,(T,X1,X2)) is non empty set
Y1 \/ (Y2 /\ Y1) is Element of K10( the carrier of T)
the carrier of (T,C2,(T,X1,X2)) is non empty set
A2 /\ (Y2 \/ Y1) is Element of K10( the carrier of T)
(A2 \/ A1) /\ (Y2 \/ Y1) is Element of K10( the carrier of T)
A1 /\ (Y2 \/ Y1) is Element of K10( the carrier of T)
(A2 /\ (Y2 \/ Y1)) \/ (A1 /\ (Y2 \/ Y1)) is Element of K10( the carrier of T)
(A2 /\ (Y2 \/ Y1)) \/ {} is set
c₁₀ is non empty TopSpace-like (T) SubSpace of T
(T,(T,C2,C1),c₁₀) is non empty strict TopSpace-like SubSpace of T
(T,c₁₀,(T,X1,X2)) is non empty strict TopSpace-like SubSpace of T
c₁₀ is non empty TopSpace-like (T) SubSpace of T
(T,(T,C2,C1),c₁₀) is non empty strict TopSpace-like SubSpace of T
(T,c₁₀,(T,X1,X2)) is non empty strict TopSpace-like SubSpace of T
the carrier of c₁₀ is non empty set
Y is Element of K10( the carrier of T)
(A2 \/ A1) \/ Y is Element of K10( the carrier of T)
A1 \/ A2 is Element of K10( the carrier of T)
(A1 \/ A2) \/ Y is Element of K10( the carrier of T)
((A1 \/ A2) \/ Y) /\ (Y2 \/ Y1) is Element of K10( the carrier of T)
A2 \/ Y is Element of K10( the carrier of T)
A1 \/ (A2 \/ Y) is Element of K10( the carrier of T)
(A1 \/ (A2 \/ Y)) /\ (Y2 \/ Y1) is Element of K10( the carrier of T)
A1 /\ (Y2 \/ Y1) is Element of K10( the carrier of T)
(A2 \/ Y) /\ (Y2 \/ Y1) is Element of K10( the carrier of T)
(A1 /\ (Y2 \/ Y1)) \/ ((A2 \/ Y) /\ (Y2 \/ Y1)) is Element of K10( the carrier of T)
{} \/ ((A2 \/ Y) /\ (Y2 \/ Y1)) is set
Y /\ (Y2 \/ Y1) is Element of K10( the carrier of T)
(A2 /\ (Y2 \/ Y1)) \/ (Y /\ (Y2 \/ Y1)) is Element of K10( the carrier of T)
the carrier of (T,c₁₀,(T,X1,X2)) is non empty set
the carrier of (T,X1,X2) is non empty set
Y2 /\ Y1 is Element of K10( the carrier of T)
Y2 \/ (Y2 /\ Y1) is Element of K10( the carrier of T)
the carrier of (T,C1,(T,X1,X2)) is non empty set
A1 /\ (Y2 \/ Y1) is Element of K10( the carrier of T)
Y2 /\ Y1 is Element of K10( the carrier of T)
(A2 \/ A1) ` is Element of K10( the carrier of T)
the carrier of T \ (A2 \/ A1) is set
c<sub>10</sub> is Element of K10( the carrier of T)
(A2 \/ A1) \/ c<sub>10</sub> is Element of K10( the carrier of T)
c<sub>10</sub> /\ (Y2 \/ Y1) is Element of K10( the carrier of T)
Y2 /\ Y1 is Element of K10( the carrier of T)
c<sub>10</sub> is non empty TopSpace-like (T) SubSpace of T
(T,(T,C2,C1),c<sub>10</sub>) is non empty strict TopSpace-like SubSpace of T
(T,c<sub>10</sub>,(T,X1,X2)) is non empty strict TopSpace-like SubSpace of T
c<sub>10</sub> is non empty TopSpace-like (T) SubSpace of T
(T,(T,C2,C1),c<sub>10</sub>) is non empty strict TopSpace-like SubSpace of T
(T,c<sub>10</sub>,(T,X1,X2)) is non empty strict TopSpace-like SubSpace of T
the carrier of c<sub>10</sub> is non empty set
Y is Element of K10( the carrier of T)
the carrier of (T,C2,C1) \/ Y is non empty set
(A2 \/ A1) \/ Y is Element of K10( the carrier of T)
((A2 \/ A1) \/ Y) /\ (Y2 \/ Y1) is Element of K10( the carrier of T)
(A2 \/ A1) /\ (Y2 \/ Y1) is Element of K10( the carrier of T)
Y /\ (Y2 \/ Y1) is Element of K10( the carrier of T)
((A2 \/ A1) /\ (Y2 \/ Y1)) \/ (Y /\ (Y2 \/ Y1)) is Element of K10( the carrier of T)
((A2 \/ A1) /\ (Y2 \/ Y1)) \/ {} is set
the carrier of (T,c<sub>10</sub>,(T,X1,X2)) is non empty set
the carrier of (T,X1,X2) is non empty set
Y2 /\ Y1 is Element of K10( the carrier of T)
Y2 /\ Y1 is Element of K10( the carrier of T)
c<sub>10</sub> is Element of K10( the carrier of T)
Y is Element of K10( the carrier of T)
c<sub>12</sub> is Element of K10( the carrier of T)
(A2 \/ A1) \/ c<sub>12</sub> is Element of K10( the carrier of T)
c<sub>12</sub> /\ (Y2 \/ Y1) is Element of K10( the carrier of T)
C2 is non empty Element of K10( the carrier of T)
C1 is non empty Element of K10( the carrier of T)
C2 /\ (Y2 \/ Y1) is Element of K10( the carrier of T)
C1 /\ (Y2 \/ Y1) is Element of K10( the carrier of T)
C2 \/ C1 is non empty Element of K10( the carrier of T)
(C2 \/ C1) /\ (Y2 \/ Y1) is Element of K10( the carrier of T)
(C2 /\ (Y2 \/ Y1)) \/ {} is set
A1 is non empty Element of K10( the carrier of T)
A1 /\ (Y2 \/ Y1) is Element of K10( the carrier of T)
(C2 \/ C1) \/ A1 is non empty Element of K10( the carrier of T)
A1 is non empty Element of K10( the carrier of T)
A1 /\ (Y2 \/ Y1) is Element of K10( the carrier of T)
(C2 \/ C1) \/ A1 is non empty Element of K10( the carrier of T)
C1 \/ C2 is non empty Element of K10( the carrier of T)
(C1 \/ C2) \/ A1 is non empty Element of K10( the carrier of T)
((C1 \/ C2) \/ A1) /\ (Y2 \/ Y1) is Element of K10( the carrier of T)
C2 \/ A1 is non empty Element of K10( the carrier of T)
C1 \/ (C2 \/ A1) is non empty Element of K10( the carrier of T)
(C1 \/ (C2 \/ A1)) /\ (Y2 \/ Y1) is Element of K10( the carrier of T)
(C2 \/ A1) /\ (Y2 \/ Y1) is Element of K10( the carrier of T)
{} \/ ((C2 \/ A1) /\ (Y2 \/ Y1)) is set
(C2 /\ (Y2 \/ Y1)) \/ (A1 /\ (Y2 \/ Y1)) is Element of K10( the carrier of T)
Y2 \/ (Y2 /\ Y1) is Element of K10( the carrier of T)
(C2 \/ C1) /\ (Y2 \/ Y1) is Element of K10( the carrier of T)
{} \/ (C1 /\ (Y2 \/ Y1)) is set
A1 is non empty Element of K10( the carrier of T)
A1 /\ (Y2 \/ Y1) is Element of K10( the carrier of T)
(C2 \/ C1) \/ A1 is non empty Element of K10( the carrier of T)
A1 is non empty Element of K10( the carrier of T)
A1 /\ (Y2 \/ Y1) is Element of K10( the carrier of T)
(C2 \/ C1) \/ A1 is non empty Element of K10( the carrier of T)
((C2 \/ C1) \/ A1) /\ (Y2 \/ Y1) is Element of K10( the carrier of T)
C1 \/ A1 is non empty Element of K10( the carrier of T)
C2 \/ (C1 \/ A1) is non empty Element of K10( the carrier of T)
(C2 \/ (C1 \/ A1)) /\ (Y2 \/ Y1) is Element of K10( the carrier of T)
(C1 \/ A1) /\ (Y2 \/ Y1) is Element of K10( the carrier of T)
{} \/ ((C1 \/ A1) /\ (Y2 \/ Y1)) is set
(C1 /\ (Y2 \/ Y1)) \/ (A1 /\ (Y2 \/ Y1)) is Element of K10( the carrier of T)
Y1 \/ (Y2 /\ Y1) 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
(T,A1,(T,X1,X2)) is non empty strict TopSpace-like SubSpace of T
the carrier of (T,A1,(T,X1,X2)) is non empty set
A2 is non empty strict TopSpace-like closed SubSpace of T
the carrier of A2 is non empty set
(T,A2,A1) is non empty strict TopSpace-like SubSpace of T
the carrier of (T,A2,A1) is non empty set
c<sub>10</sub> is non empty Element of K10( the carrier of T)
c<sub>10</sub> /\ (Y2 \/ Y1) is Element of K10( the carrier of T)
(C2 \/ C1) \/ c<sub>10</sub> is non empty Element of K10( the carrier of T)
c<sub>10</sub> is non empty Element of K10( the carrier of T)
c<sub>10</sub> /\ (Y2 \/ Y1) is Element of K10( the carrier of T)
(C2 \/ C1) \/ c<sub>10</sub> is non empty Element of K10( the carrier of T)
Y is non empty strict TopSpace-like (T) SubSpace of T
the carrier of Y is non empty set
((C2 \/ C1) \/ c<sub>10</sub>) /\ (Y2 \/ Y1) is Element of K10( the carrier of T)
(C2 \/ C1) /\ (Y2 \/ Y1) is Element of K10( the carrier of T)
((C2 \/ C1) /\ (Y2 \/ Y1)) \/ {} is set
(T,Y,(T,X1,X2)) is non empty strict TopSpace-like SubSpace of T
the carrier of (T,Y,(T,X1,X2)) is non empty set
(T,(T,A2,A1),Y) is non empty strict TopSpace-like SubSpace of T
the carrier of (T,X1,X2) is non empty set
the carrier of (T,A2,A1) \/ c<sub>10</sub> is non empty set
the carrier of (T,(T,A2,A1),Y) is non empty set
(T,A2,(T,X1,X2)) is non empty strict TopSpace-like SubSpace of T
the carrier of (T,A2,(T,X1,X2)) is non empty set
c<sub>10</sub> is non empty TopSpace-like (T) SubSpace of T
(T,(T,A2,A1),c<sub>10</sub>) is non empty strict TopSpace-like SubSpace of T
(T,c<sub>10</sub>,(T,X1,X2)) is non empty strict TopSpace-like SubSpace of T
C2 is non empty TopSpace-like closed SubSpace of T
(T,C2,(T,X1,X2)) is non empty strict TopSpace-like SubSpace of T
C1 is non empty TopSpace-like closed SubSpace of T
(T,C1,(T,X1,X2)) is non empty strict TopSpace-like SubSpace of T
(T,C2,C1) is non empty strict TopSpace-like SubSpace of T
A1 is non empty TopSpace-like (T) SubSpace of T
(T,(T,C2,C1),A1) is non empty strict TopSpace-like SubSpace of T
(T,A1,(T,X1,X2)) is non empty strict TopSpace-like SubSpace of T
C2 is non empty TopSpace-like closed SubSpace of T
(T,C2,(T,X1,X2)) is non empty strict TopSpace-like SubSpace of T
C1 is non empty TopSpace-like closed SubSpace of T
(T,C1,(T,X1,X2)) is non empty strict TopSpace-like SubSpace of T
(T,C2,C1) is non empty strict TopSpace-like SubSpace of T
A1 is non empty TopSpace-like (T) SubSpace of T
(T,(T,C2,C1),A1) is non empty strict TopSpace-like SubSpace of T
(T,A1,(T,X1,X2)) is non empty strict TopSpace-like SubSpace of T
A2 is non empty TopSpace-like closed SubSpace of T
(T,A2,(T,X1,X2)) is non empty strict TopSpace-like SubSpace of T
c<sub>10</sub> is non empty TopSpace-like closed SubSpace of T
(T,c<sub>10</sub>,(T,X1,X2)) is non empty strict TopSpace-like SubSpace of T
(T,A2,c<sub>10</sub>) is non empty strict TopSpace-like SubSpace of T
Y is non empty TopSpace-like (T) SubSpace of T
(T,(T,A2,c<sub>10</sub>),Y) is non empty strict TopSpace-like SubSpace of T
(T,Y,(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
(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 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 non empty TopSpace-like (T) SubSpace of T
(T,(T,C2,C1),A1) is non empty strict TopSpace-like SubSpace of T
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
the carrier of C1 is non empty set
the carrier of C2 is non empty set
A2 is Element of K10( the carrier of T)
A1 is Element of K10( the carrier of T)
A2 \/ A1 is Element of K10( the carrier of T)
Y2 /\ Y1 is Element of K10( the carrier of T)
{} T is empty open closed Element of K10( the carrier of T)
(A2 \/ A1) \/ ({} T) is Element of K10( the carrier of T)
A2 is Element of K10( the carrier of T)
A1 is Element of K10( the carrier of T)
A2 \/ A1 is Element of K10( the carrier of T)
Y2 /\ Y1 is Element of K10( the carrier of T)
c<sub>10</sub> is non empty TopSpace-like (T) SubSpace of T
(T,(T,C2,C1),c<sub>10</sub>) is non empty strict TopSpace-like SubSpace of T
c<sub>10</sub> is non empty TopSpace-like (T) SubSpace of T
(T,(T,C2,C1),c<sub>10</sub>) is non empty strict TopSpace-like SubSpace of T
the carrier of c<sub>10</sub> is non empty set
the carrier of (T,X1,X2) is non empty set
Y is Element of K10( the carrier of T)
the carrier of (T,C2,C1) is non empty set
the carrier of (T,C2,C1) \/ Y is non empty set
(A2 \/ A1) \/ Y is Element of K10( the carrier of T)
A2 is Element of K10( the carrier of T)
A1 is Element of K10( the carrier of T)
A2 \/ A1 is Element of K10( the carrier of T)
Y2 /\ Y1 is Element of K10( the carrier of T)
A2 is Element of K10( the carrier of T)
A1 is Element of K10( the carrier of T)
A2 \/ A1 is Element of K10( the carrier of T)
Y2 /\ Y1 is Element of K10( the carrier of T)
c<sub>10</sub> is Element of K10( the carrier of T)
Y is Element of K10( the carrier of T)
c<sub>12</sub> is Element of K10( the carrier of T)
(A2 \/ A1) \/ c<sub>12</sub> is Element of K10( the carrier of T)
C2 is non empty Element of K10( the carrier of T)
C1 is non empty Element of K10( the carrier of T)
C2 \/ C1 is non empty 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,A2,A1) is non empty strict TopSpace-like SubSpace of T
c<sub>10</sub> is non empty Element of K10( the carrier of T)
(C2 \/ C1) \/ c<sub>10</sub> is non empty Element of K10( the carrier of T)
c<sub>10</sub> is non empty Element of K10( the carrier of T)
(C2 \/ C1) \/ c<sub>10</sub> is non empty Element of K10( the carrier of T)
the carrier of (T,X1,X2) is non empty set
Y is non empty strict TopSpace-like (T) SubSpace of T
the carrier of Y is non empty set
(T,(T,A2,A1),Y) is non empty strict TopSpace-like SubSpace of T
the carrier of (T,A2,A1) is non empty set
the carrier of (T,A2,A1) \/ c<sub>10</sub> is non empty set
the carrier of (T,(T,A2,A1),Y) is non empty set
c<sub>10</sub> is non empty TopSpace-like (T) SubSpace of T
(T,(T,A2,A1),c<sub>10</sub>) is non empty strict TopSpace-like SubSpace of T
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 non empty TopSpace-like (T) SubSpace of T
(T,(T,C2,C1),A1) is non empty strict TopSpace-like SubSpace of T
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 non empty TopSpace-like (T) SubSpace of T
(T,(T,C2,C1),A1) is non empty strict TopSpace-like SubSpace of T
A2 is non empty TopSpace-like closed SubSpace of T
c<sub>10</sub> is non empty TopSpace-like closed SubSpace of T
(T,A2,c<sub>10</sub>) is non empty strict TopSpace-like SubSpace of T
Y is non empty TopSpace-like (T) SubSpace of T
(T,(T,A2,c<sub>10</sub>),Y) 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
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
the carrier of T is non empty 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 non empty strict 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
the carrier of X2 is non empty set
the carrier of X1 is non empty set
[#] T is non empty non proper open closed Element of K10( the carrier of T)
C2 is non empty TopSpace-like (T) SubSpace of T
(T,C2,(T,X1,X2)) is non empty strict TopSpace-like SubSpace of T
C1 is non empty TopSpace-like (T) SubSpace of T
(T,C1,(T,X1,X2)) is non empty strict TopSpace-like SubSpace of T
(T,C2,C1) is non empty strict TopSpace-like SubSpace of T
A1 is non empty TopSpace-like closed SubSpace of T
(T,(T,C2,C1),A1) is non empty strict TopSpace-like SubSpace of T
(T,A1,(T,X1,X2)) is non empty strict TopSpace-like SubSpace of T
C2 is non empty TopSpace-like (T) SubSpace of T
(T,C2,(T,X1,X2)) is non empty strict TopSpace-like SubSpace of T
C1 is non empty TopSpace-like (T) SubSpace of T
(T,C1,(T,X1,X2)) is non empty strict TopSpace-like SubSpace of T
(T,C2,C1) is non empty strict TopSpace-like SubSpace of T
the carrier of C1 is non empty set
the carrier of C2 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)
the carrier of (T,C2,C1) is non empty set
A2 is Element of K10( the carrier of T)
A1 is Element of K10( the carrier of T)
A2 \/ A1 is Element of K10( the carrier of T)
(A2 \/ A1) /\ (Y2 \/ Y1) is Element of K10( the carrier of T)
A2 /\ (Y2 \/ Y1) is Element of K10( the carrier of T)
A1 /\ (Y2 \/ Y1) is Element of K10( the carrier of T)
(A2 /\ (Y2 \/ Y1)) \/ (A1 /\ (Y2 \/ Y1)) is Element of K10( the carrier of T)
{} \/ (A1 /\ (Y2 \/ Y1)) is set
the carrier of (T,C1,(T,X1,X2)) is non empty set
c<sub>10</sub> is non empty TopSpace-like closed SubSpace of T
(T,(T,C2,C1),c<sub>10</sub>) is non empty strict TopSpace-like SubSpace of T
(T,c<sub>10</sub>,(T,X1,X2)) is non empty strict TopSpace-like SubSpace of T
c<sub>10</sub> is non empty TopSpace-like closed SubSpace of T
(T,(T,C2,C1),c<sub>10</sub>) is non empty strict TopSpace-like SubSpace of T
(T,c<sub>10</sub>,(T,X1,X2)) is non empty strict TopSpace-like SubSpace of T
the carrier of c<sub>10</sub> is non empty set
Y is Element of K10( the carrier of T)
(A2 \/ A1) \/ Y is Element of K10( the carrier of T)
((A2 \/ A1) \/ Y) /\ (Y2 \/ Y1) is Element of K10( the carrier of T)
A1 \/ Y is Element of K10( the carrier of T)
A2 \/ (A1 \/ Y) is Element of K10( the carrier of T)
(A2 \/ (A1 \/ Y)) /\ (Y2 \/ Y1) is Element of K10( the carrier of T)
A2 /\ (Y2 \/ Y1) is Element of K10( the carrier of T)
(A1 \/ Y) /\ (Y2 \/ Y1) is Element of K10( the carrier of T)
(A2 /\ (Y2 \/ Y1)) \/ ((A1 \/ Y) /\ (Y2 \/ Y1)) is Element of K10( the carrier of T)
{} \/ ((A1 \/ Y) /\ (Y2 \/ Y1)) is set
A1 /\ (Y2 \/ Y1) is Element of K10( the carrier of T)
Y /\ (Y2 \/ Y1) is Element of K10( the carrier of T)
(A1 /\ (Y2 \/ Y1)) \/ (Y /\ (Y2 \/ Y1)) is Element of K10( the carrier of T)
the carrier of (T,c<sub>10</sub>,(T,X1,X2)) is non empty set
the carrier of (T,X1,X2) is non empty set
Y2 /\ Y1 is Element of K10( the carrier of T)
the carrier of (T,C1,(T,X1,X2)) is non empty set
the carrier of (T,C1,(T,X1,X2)) is non empty set
Y1 \/ (Y2 /\ Y1) is Element of K10( the carrier of T)
the carrier of (T,C2,(T,X1,X2)) is non empty set
A2 /\ (Y2 \/ Y1) is Element of K10( the carrier of T)
(A2 \/ A1) /\ (Y2 \/ Y1) is Element of K10( the carrier of T)
A1 /\ (Y2 \/ Y1) is Element of K10( the carrier of T)
(A2 /\ (Y2 \/ Y1)) \/ (A1 /\ (Y2 \/ Y1)) is Element of K10( the carrier of T)
(A2 /\ (Y2 \/ Y1)) \/ {} is set
c<sub>10</sub> is non empty TopSpace-like closed SubSpace of T
(T,(T,C2,C1),c<sub>10</sub>) is non empty strict TopSpace-like SubSpace of T
(T,c<sub>10</sub>,(T,X1,X2)) is non empty strict TopSpace-like SubSpace of T
c<sub>10</sub> is non empty TopSpace-like closed SubSpace of T
(T,(T,C2,C1),c<sub>10</sub>) is non empty strict TopSpace-like SubSpace of T
(T,c<sub>10</sub>,(T,X1,X2)) is non empty strict TopSpace-like SubSpace of T
the carrier of c<sub>10</sub> is non empty set
Y is Element of K10( the carrier of T)
(A2 \/ A1) \/ Y is Element of K10( the carrier of T)
A1 \/ A2 is Element of K10( the carrier of T)
(A1 \/ A2) \/ Y is Element of K10( the carrier of T)
((A1 \/ A2) \/ Y) /\ (Y2 \/ Y1) is Element of K10( the carrier of T)
A2 \/ Y is Element of K10( the carrier of T)
A1 \/ (A2 \/ Y) is Element of K10( the carrier of T)
(A1 \/ (A2 \/ Y)) /\ (Y2 \/ Y1) is Element of K10( the carrier of T)
A1 /\ (Y2 \/ Y1) is Element of K10( the carrier of T)
(A2 \/ Y) /\ (Y2 \/ Y1) is Element of K10( the carrier of T)
(A1 /\ (Y2 \/ Y1)) \/ ((A2 \/ Y) /\ (Y2 \/ Y1)) is Element of K10( the carrier of T)
{} \/ ((A2 \/ Y) /\ (Y2 \/ Y1)) is set
Y /\ (Y2 \/ Y1) is Element of K10( the carrier of T)
(A2 /\ (Y2 \/ Y1)) \/ (Y /\ (Y2 \/ Y1)) is Element of K10( the carrier of T)
the carrier of (T,c<sub>10</sub>,(T,X1,X2)) is non empty set
the carrier of (T,X1,X2) is non empty set
Y2 /\ Y1 is Element of K10( the carrier of T)
Y2 \/ (Y2 /\ Y1) is Element of K10( the carrier of T)
the carrier of (T,C1,(T,X1,X2)) is non empty set
A1 /\ (Y2 \/ Y1) is Element of K10( the carrier of T)
Y2 /\ Y1 is Element of K10( the carrier of T)
(A2 \/ A1) ` is Element of K10( the carrier of T)
the carrier of T \ (A2 \/ A1) is set
c₁₀ is Element of K10( the carrier of T)
(A2 \/ A1) \/ c₁₀ is Element of K10( the carrier of T)
c₁₀ /\ (Y2 \/ Y1) is Element of K10( the carrier of T)
Y2 /\ Y1 is Element of K10( the carrier of T)
c₁₀ is non empty TopSpace-like closed SubSpace of T
(T,(T,C2,C1),c₁₀) is non empty strict TopSpace-like SubSpace of T
(T,c₁₀,(T,X1,X2)) is non empty strict TopSpace-like SubSpace of T
c₁₀ is non empty TopSpace-like closed SubSpace of T
(T,(T,C2,C1),c₁₀) is non empty strict TopSpace-like SubSpace of T
(T,c₁₀,(T,X1,X2)) is non empty strict TopSpace-like SubSpace of T
the carrier of c₁₀ is non empty set
Y is Element of K10( the carrier of T)
the carrier of (T,C2,C1) \/ Y is non empty set
(A2 \/ A1) \/ Y is Element of K10( the carrier of T)
((A2 \/ A1) \/ Y) /\ (Y2 \/ Y1) is Element of K10( the carrier of T)
(A2 \/ A1) /\ (Y2 \/ Y1) is Element of K10( the carrier of T)
Y /\ (Y2 \/ Y1) is Element of K10( the carrier of T)
((A2 \/ A1) /\ (Y2 \/ Y1)) \/ (Y /\ (Y2 \/ Y1)) is Element of K10( the carrier of T)
((A2 \/ A1) /\ (Y2 \/ Y1)) \/ {} is set
the carrier of (T,c₁₀,(T,X1,X2)) is non empty set
the carrier of (T,X1,X2) is non empty set
Y2 /\ Y1 is Element of K10( the carrier of T)
Y2 /\ Y1 is Element of K10( the carrier of T)
c₁₀ is Element of K10( the carrier of T)
Y is Element of K10( the carrier of T)
c₁₂ is Element of K10( the carrier of T)
(A2 \/ A1) \/ c₁₂ is Element of K10( the carrier of T)
c₁₂ /\ (Y2 \/ Y1) is Element of K10( the carrier of T)
C2 is non empty Element of K10( the carrier of T)
C1 is non empty Element of K10( the carrier of T)
C2 /\ (Y2 \/ Y1) is Element of K10( the carrier of T)
C1 /\ (Y2 \/ Y1) is Element of K10( the carrier of T)
C2 \/ C1 is non empty Element of K10( the carrier of T)
(C2 \/ C1) /\ (Y2 \/ Y1) is Element of K10( the carrier of T)
(C2 /\ (Y2 \/ Y1)) \/ {} is set
A1 is non empty Element of K10( the carrier of T)
A1 /\ (Y2 \/ Y1) is Element of K10( the carrier of T)
(C2 \/ C1) \/ A1 is non empty Element of K10( the carrier of T)
A1 is non empty Element of K10( the carrier of T)
A1 /\ (Y2 \/ Y1) is Element of K10( the carrier of T)
(C2 \/ C1) \/ A1 is non empty Element of K10( the carrier of T)
C1 \/ C2 is non empty Element of K10( the carrier of T)
(C1 \/ C2) \/ A1 is non empty Element of K10( the carrier of T)
((C1 \/ C2) \/ A1) /\ (Y2 \/ Y1) is Element of K10( the carrier of T)
C2 \/ A1 is non empty Element of K10( the carrier of T)
C1 \/ (C2 \/ A1) is non empty Element of K10( the carrier of T)
(C1 \/ (C2 \/ A1)) /\ (Y2 \/ Y1) is Element of K10( the carrier of T)
(C2 \/ A1) /\ (Y2 \/ Y1) is Element of K10( the carrier of T)
{} \/ ((C2 \/ A1) /\ (Y2 \/ Y1)) is set
(C2 /\ (Y2 \/ Y1)) \/ (A1 /\ (Y2 \/ Y1)) is Element of K10( the carrier of T)
Y2 \/ (Y2 /\ Y1) is Element of K10( the carrier of T)
(C2 \/ C1) /\ (Y2 \/ Y1) is Element of K10( the carrier of T)
{} \/ (C1 /\ (Y2 \/ Y1)) is set
A1 is non empty Element of K10( the carrier of T)
A1 /\ (Y2 \/ Y1) is Element of K10( the carrier of T)
(C2 \/ C1) \/ A1 is non empty Element of K10( the carrier of T)
A1 is non empty Element of K10( the carrier of T)
A1 /\ (Y2 \/ Y1) is Element of K10( the carrier of T)
(C2 \/ C1) \/ A1 is non empty Element of K10( the carrier of T)
((C2 \/ C1) \/ A1) /\ (Y2 \/ Y1) is Element of K10( the carrier of T)
C1 \/ A1 is non empty Element of K10( the carrier of T)
C2 \/ (C1 \/ A1) is non empty Element of K10( the carrier of T)
(C2 \/ (C1 \/ A1)) /\ (Y2 \/ Y1) is Element of K10( the carrier of T)
(C1 \/ A1) /\ (Y2 \/ Y1) is Element of K10( the carrier of T)
{} \/ ((C1 \/ A1) /\ (Y2 \/ Y1)) is set
(C1 /\ (Y2 \/ Y1)) \/ (A1 /\ (Y2 \/ Y1)) is Element of K10( the carrier of T)
Y1 \/ (Y2 /\ Y1) 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
(T,A1,(T,X1,X2)) is non empty strict TopSpace-like SubSpace of T
the carrier of (T,A1,(T,X1,X2)) is non empty set
A2 is non empty strict TopSpace-like (T) SubSpace of T
the carrier of A2 is non empty set
(T,A2,A1) is non empty strict TopSpace-like SubSpace of T
the carrier of (T,A2,A1) is non empty set
c₁₀ is non empty Element of K10( the carrier of T)
c₁₀ /\ (Y2 \/ Y1) is Element of K10( the carrier of T)
(C2 \/ C1) \/ c₁₀ is non empty Element of K10( the carrier of T)
c₁₀ is non empty Element of K10( the carrier of T)
c₁₀ /\ (Y2 \/ Y1) is Element of K10( the carrier of T)
(C2 \/ C1) \/ c₁₀ is non empty Element of K10( the carrier of T)
Y is non empty strict TopSpace-like closed SubSpace of T
the carrier of Y is non empty set
((C2 \/ C1) \/ c₁₀) /\ (Y2 \/ Y1) is Element of K10( the carrier of T)
(C2 \/ C1) /\ (Y2 \/ Y1) is Element of K10( the carrier of T)
((C2 \/ C1) /\ (Y2 \/ Y1)) \/ {} is set
(T,Y,(T,X1,X2)) is non empty strict TopSpace-like SubSpace of T
the carrier of (T,Y,(T,X1,X2)) is non empty set
(T,(T,A2,A1),Y) is non empty strict TopSpace-like SubSpace of T
the carrier of (T,X1,X2) is non empty set
the carrier of (T,A2,A1) \/ c₁₀ is non empty set
the carrier of (T,(T,A2,A1),Y) is non empty set
(T,A2,(T,X1,X2)) is non empty strict TopSpace-like SubSpace of T
the carrier of (T,A2,(T,X1,X2)) is non empty set
c₁₀ is non empty TopSpace-like closed SubSpace of T
(T,(T,A2,A1),c₁₀) is non empty strict TopSpace-like SubSpace of T
(T,c₁₀,(T,X1,X2)) is non empty strict TopSpace-like SubSpace of T
C2 is non empty TopSpace-like (T) SubSpace of T
(T,C2,(T,X1,X2)) is non empty strict TopSpace-like SubSpace of T
C1 is non empty TopSpace-like (T) SubSpace of T
(T,C1,(T,X1,X2)) is non empty strict TopSpace-like SubSpace of T
(T,C2,C1) is non empty strict TopSpace-like SubSpace of T
A1 is non empty TopSpace-like closed SubSpace of T
(T,(T,C2,C1),A1) is non empty strict TopSpace-like SubSpace of T
(T,A1,(T,X1,X2)) is non empty strict TopSpace-like SubSpace of T
C2 is non empty TopSpace-like (T) SubSpace of T
(T,C2,(T,X1,X2)) is non empty strict TopSpace-like SubSpace of T
C1 is non empty TopSpace-like (T) SubSpace of T
(T,C1,(T,X1,X2)) is non empty strict TopSpace-like SubSpace of T
(T,C2,C1) is non empty strict TopSpace-like SubSpace of T
A1 is non empty TopSpace-like closed SubSpace of T
(T,(T,C2,C1),A1) is non empty strict TopSpace-like SubSpace of T
(T,A1,(T,X1,X2)) is non empty strict TopSpace-like SubSpace of T
A2 is non empty TopSpace-like (T) SubSpace of T
(T,A2,(T,X1,X2)) is non empty strict TopSpace-like SubSpace of T
c₁₀ is non empty TopSpace-like (T) SubSpace of T
(T,c₁₀,(T,X1,X2)) is non empty strict TopSpace-like SubSpace of T
(T,A2,c₁₀) is non empty strict TopSpace-like SubSpace of T
Y is non empty TopSpace-like closed SubSpace of T
(T,(T,A2,c₁₀),Y) is non empty strict TopSpace-like SubSpace of T
(T,Y,(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
(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 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 non empty TopSpace-like closed SubSpace of T
(T,(T,C2,C1),A1) is non empty strict TopSpace-like SubSpace of T
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
the carrier of C1 is non empty set
the carrier of C2 is non empty set
A2 is Element of K10( the carrier of T)
A1 is Element of K10( the carrier of T)
A2 \/ A1 is Element of K10( the carrier of T)
Y2 /\ Y1 is Element of K10( the carrier of T)
{} T is empty open closed Element of K10( the carrier of T)
(A2 \/ A1) \/ ({} T) is Element of K10( the carrier of T)
A2 is Element of K10( the carrier of T)
A1 is Element of K10( the carrier of T)
A2 \/ A1 is Element of K10( the carrier of T)
Y2 /\ Y1 is Element of K10( the carrier of T)
c₁₀ is non empty TopSpace-like closed SubSpace of T
(T,(T,C2,C1),c₁₀) is non empty strict TopSpace-like SubSpace of T
c₁₀ is non empty TopSpace-like closed SubSpace of T
(T,(T,C2,C1),c₁₀) is non empty strict TopSpace-like SubSpace of T
the carrier of c₁₀ is non empty set
the carrier of (T,X1,X2) is non empty set
Y is Element of K10( the carrier of T)
the carrier of (T,C2,C1) is non empty set
the carrier of (T,C2,C1) \/ Y is non empty set
(A2 \/ A1) \/ Y is Element of K10( the carrier of T)
A2 is Element of K10( the carrier of T)
A1 is Element of K10( the carrier of T)
A2 \/ A1 is Element of K10( the carrier of T)
Y2 /\ Y1 is Element of K10( the carrier of T)
A2 is Element of K10( the carrier of T)
A1 is Element of K10( the carrier of T)
A2 \/ A1 is Element of K10( the carrier of T)
Y2 /\ Y1 is Element of K10( the carrier of T)
c₁₀ is Element of K10( the carrier of T)
Y is Element of K10( the carrier of T)
c₁₂ is Element of K10( the carrier of T)
(A2 \/ A1) \/ c₁₂ is Element of K10( the carrier of T)
C2 is non empty Element of K10( the carrier of T)
C1 is non empty Element of K10( the carrier of T)
C2 \/ C1 is non empty 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,A2,A1) is non empty strict TopSpace-like SubSpace of T
c₁₀ is non empty Element of K10( the carrier of T)
(C2 \/ C1) \/ c₁₀ is non empty Element of K10( the carrier of T)
c₁₀ is non empty Element of K10( the carrier of T)
(C2 \/ C1) \/ c₁₀ is non empty Element of K10( the carrier of T)
the carrier of (T,X1,X2) is non empty set
Y is non empty strict TopSpace-like closed SubSpace of T
the carrier of Y is non empty set
(T,(T,A2,A1),Y) is non empty strict TopSpace-like SubSpace of T
the carrier of (T,A2,A1) is non empty set
the carrier of (T,A2,A1) \/ c₁₀ is non empty set
the carrier of (T,(T,A2,A1),Y) is non empty set
c₁₀ is non empty TopSpace-like closed SubSpace of T
(T,(T,A2,A1),c₁₀) is non empty strict TopSpace-like SubSpace of T
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 non empty TopSpace-like closed SubSpace of T
(T,(T,C2,C1),A1) is non empty strict TopSpace-like SubSpace of T
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 non empty TopSpace-like closed SubSpace of T
(T,(T,C2,C1),A1) is non empty strict TopSpace-like SubSpace of T
A2 is non empty TopSpace-like (T) SubSpace of T
c₁₀ is non empty TopSpace-like (T) SubSpace of T
(T,A2,c₁₀) is non empty strict TopSpace-like SubSpace of T
Y is non empty TopSpace-like closed SubSpace of T
(T,(T,A2,c₁₀),Y) 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
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
Y1 is non empty TopSpace-like (T) SubSpace of T
Y2 is non empty TopSpace-like (T) SubSpace of T
(T,Y1,Y2) is non empty strict TopSpace-like SubSpace of T
Y1 is non empty TopSpace-like SubSpace of T
Y2 is non empty TopSpace-like SubSpace of T
(T,Y1,Y2) 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 Y2 is non empty set
the carrier of Y1 is non empty set
A1 is Element of K10( the carrier of T)
the carrier of X1 is non empty set
A2 is Element of K10( the carrier of T)
the carrier of X2 is non empty set
C1 is Element of K10( the carrier of T)
C2 is Element of K10( the carrier of T)
A1 \/ A2 is Element of K10( the carrier of T)
C1 is Element of K10( the carrier of T)
C2 is Element of K10( the carrier of T)
C1 /\ C2 is Element of K10( the carrier of T)
the carrier of (T,Y1,Y2) is non empty set
the carrier of (T,X1,X2) is non empty set
c₁₀ is Element of K10( the carrier of T)
Y is Element of K10( the carrier of T)
c₁₀ /\ Y is Element of K10( the carrier of 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
T | ([#] T) is strict SubSpace of T
the topology of T is Element of K10(K10( the carrier of T))
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