K96() is set
K10(K96()) is non empty set
{} is set
the empty set is empty set
1 is non empty set
union {} is set
T is TopStruct
the carrier of T is set
K10( the carrier of T) is non empty set
K10(K10( the carrier of T)) is non empty set
A is Element of K10( the carrier of T)
F is Element of K10(K10( the carrier of T))
union F is Element of K10( the carrier of T)
X is Element of K10( the carrier of T)
X is Element of K10( the carrier of T)
F is Element of K10( the carrier of T)
X is Element of K10( the carrier of T)
X is Element of K10(K10( the carrier of T))
union X is Element of K10( the carrier of T)
X is Element of K10(K10( the carrier of T))
union X is Element of K10( the carrier of T)
x is Element of K10(K10( the carrier of T))
union x is Element of K10( the carrier of T)
x is Element of K10(K10( the carrier of T))
union x is Element of K10( the carrier of T)
Y is set
X is set
A2 is Element of K10( the carrier of T)
X is set
A2 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 non empty set
A is Element of K10( the carrier of T)
(T,A) is Element of K10( the carrier of T)
F is Element of K10( the carrier of T)
K10(K10( the carrier of T)) is non empty set
X is Element of K10(K10( the carrier of T))
union X is Element of K10( the carrier of T)
X is set
meet X 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 non empty set
A is Element of K10( the carrier of T)
(T,A) is Element of K10( the carrier of T)
K10(K10( the carrier of T)) is non empty set
F is Element of K10(K10( the carrier of T))
union F is Element of K10( the carrier of T)
X is Element of K10( the carrier of T)
X is Element of K10( the carrier of T)
T is non empty TopSpace-like TopStruct
{} T is empty proper closed connected Element of K10( the carrier of T)
the carrier of T is non empty set
K10( the carrier of T) is non empty set
(T,({} T)) is Element of K10( the carrier of T)
K10(K10( the carrier of T)) is non empty set
A is Element of K10(K10( the carrier of T))
F is Element of K10( the carrier of T)
X is Element of K10( the carrier of T)
F is set
X is Element of the carrier of T
Component_of X is non empty connected Element of K10( the carrier of T)
X is set
x is set
X is set
union A 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 non empty set
A is Element of K10( the carrier of T)
(T,A) is Element of K10( the carrier of T)
{} T is empty proper closed connected Element of K10( the carrier of T)
T is TopSpace-like TopStruct
the carrier of T is set
K10( the carrier of T) is non empty set
A is Element of K10( the carrier of T)
(T,A) is Element of K10( the carrier of T)
K10(K10( the carrier of T)) is non empty set
F is Element of K10(K10( the carrier of T))
union F is Element of K10( the carrier of T)
X is set
meet F is Element of K10( the carrier of T)
{} T is empty closed connected Element of K10( the carrier of T)
X 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 non empty set
A is Element of K10( the carrier of T)
F is Element of K10( the carrier of T)
(T,A) is Element of K10( the carrier of T)
K10(K10( the carrier of T)) is non empty set
X is Element of K10(K10( the carrier of T))
union X 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 non empty set
A is Element of K10( the carrier of T)
(T,A) is Element of K10( the carrier of T)
{} T is empty proper closed connected 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 non empty set
A is Element of K10( the carrier of T)
F is Element of K10( the carrier of T)
(T,F) is Element of K10( the carrier of T)
F is Element of K10( the carrier of T)
(T,F) is Element of K10( the carrier of T)
X is Element of K10( the carrier of T)
F is Element of K10( the carrier of T)
(T,F) is Element of K10( the carrier of T)
X is Element of K10( the carrier of T)
(T,X) 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 non empty set
A is Element of K10( the carrier of T)
(T,A) 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 non empty set
A is Element of K10( the carrier of T)
F is Element of K10( the carrier of T)
(T,F) 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 non empty set
A is Element of K10( the carrier of T)
(T,A) is Element of K10( the carrier of T)
(T,(T,A)) 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 non empty set
A is Element of K10( the carrier of T)
F is Element of K10( the carrier of T)
(T,A) is Element of K10( the carrier of T)
(T,F) is Element of K10( the carrier of T)
K10(K10( the carrier of T)) is non empty set
X is Element of K10(K10( the carrier of T))
union X is Element of K10( the carrier of T)
K10(K10( the carrier of T)) is non empty set
X is Element of K10(K10( the carrier of T))
union X 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 non empty set
A is Element of K10( the carrier of T)
F is Element of K10( the carrier of T)
(T,A) is Element of K10( the carrier of T)
(T,F) 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 non empty set
A is Element of K10( the carrier of T)
(T,A) is Element of K10( the carrier of T)
F is Element of K10( the carrier of T)
A \/ F is Element of K10( the carrier of T)
(T,(A \/ F)) 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 non empty set
A is Element of K10( the carrier of T)
(T,A) is Element of K10( the carrier of T)
F is Element of the carrier of T
Component_of F is non empty connected 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 non empty set
A is Element of K10( the carrier of T)
F is Element of K10( the carrier of T)
A \/ F is Element of K10( the carrier of T)
(T,A) is Element of K10( the carrier of T)
(T,F) is Element of K10( the carrier of T)
X is Element of K10( the carrier of T)
X is Element of K10( the carrier of T)
X /\ X is Element of K10( the carrier of T)
X \/ X is Element of K10( the carrier of T)
(T,X) is Element of K10( the carrier of T)
A /\ F 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 non empty set
A is Element of K10( the carrier of T)
Cl A is Element of K10( the carrier of T)
(T,A) 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 non empty set
A is Element of K10( the carrier of T)
F is Element of K10( the carrier of T)
(T,F) is Element of K10( the carrier of T)
A /\ F is Element of K10( the carrier of T)
A /\ (T,F) is Element of K10( the carrier of T)
X is Element of the carrier of T
Component_of X is non empty connected Element of K10( the carrier of T)
(T,A) is Element of K10( the carrier of T)
(T,(T,F)) is Element of K10( the carrier of T)
(T,F) /\ F is Element of K10( the carrier of T)
T is TopStruct
the carrier of T is set
K10( the carrier of T) is non empty set
K10(K10( the carrier of T)) is non empty set
A is Element of K10(K10( the carrier of T))
F is Element of K10( the carrier of T)
{} T is empty connected Element of K10( the carrier of T)
T is TopStruct
the carrier of T is set
K10( the carrier of T) is non empty set
K10(K10( the carrier of T)) is non empty set
{} T is empty connected Element of K10( the carrier of T)
T is non empty TopSpace-like TopStruct
{} T is empty proper closed connected Element of K10( the carrier of T)
the carrier of T is non empty set
K10( the carrier of T) is non empty set
K10(K10( the carrier of T)) is non empty set
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
K10( the carrier of T) is non empty set
A is Element of K10( the carrier of T)
{ b1 where b1 is Element of K10( the carrier of T) : b1 is a_component } is set
bool the carrier of T is non empty Element of K10(K10( the carrier of T))
K10(K10( the carrier of T)) is non empty set
F is set
X is Element of K10( the carrier of T)
F is Element of K10(K10( the carrier of T))
X is Element of K10( the carrier of T)
X is Element of K10( the carrier of T)
union F is Element of K10( the carrier of T)
X is set
X is Element of the carrier of T
Component_of X is non empty connected 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 non empty set
A is Element of K10( the carrier of T)
F is Element of the carrier of T
Component_of F is non empty connected Element of K10( the carrier of T)
K10(K10( the carrier of T)) is non empty set
X is Element of K10(K10( the carrier of T))
union X is Element of K10( the carrier of T)
X is set
x 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 non empty set
A is Element of K10( the carrier of T)
F is Element of K10( the carrier of T)
A \/ F is Element of K10( the carrier of T)
A /\ F is Element of K10( the carrier of T)
K10(K10( the carrier of T)) is non empty set
X is Element of K10(K10( the carrier of T))
union X is Element of K10( the carrier of T)
X is Element of K10(K10( the carrier of T))
union X is Element of K10( the carrier of T)
X \/ X is Element of K10(K10( the carrier of T))
x is Element of K10( the carrier of T)
X /\ X is Element of K10(K10( the carrier of T))
x is Element of K10(K10( the carrier of T))
Y is Element of K10( the carrier of T)
union x is Element of K10( the carrier of T)
Y is set
X is set
Y3 is set
B3 is Element of K10( the carrier of T)
A2 is Element of K10( the carrier of T)
X /\ Y3 is set
Y is set
X is set
x is Element of K10(K10( the carrier of T))
union x 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 non empty set
K10(K10( the carrier of T)) is non empty set
A is Element of K10(K10( the carrier of T))
union A is Element of K10( the carrier of T)
{ b1 where b1 is Element of K10( the carrier of T) : ex b2 being Element of K10( the carrier of T) st
( b2 in A & b1 c= b2 & b1 is a_component ) } is set
bool the carrier of T is non empty Element of K10(K10( the carrier of T))
F is set
X is Element of K10( the carrier of T)
X is Element of K10( the carrier of T)
F is Element of K10(K10( the carrier of T))
X is Element of K10( the carrier of T)
X is Element of K10( the carrier of T)
x is Element of K10( the carrier of T)
union F is Element of K10( the carrier of T)
X is set
X is set
x is Element of K10( the carrier of T)
Y is Element of K10(K10( the carrier of T))
union Y is Element of K10( the carrier of T)
X is set
A2 is Element of K10( the carrier of T)
X is set
X is set
x is Element of K10( the carrier of T)
Y 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 non empty set
K10(K10( the carrier of T)) is non empty set
A is Element of K10(K10( the carrier of T))
meet A is Element of K10( the carrier of T)
{ b1 where b1 is Element of K10( the carrier of T) : ( b1 is a_component & ( for b2 being Element of K10( the carrier of T) holds
( not b2 in A or b1 c= b2 ) ) ) } is set
bool the carrier of T is non empty Element of K10(K10( the carrier of T))
F is set
X is Element of K10( the carrier of T)
F is Element of K10(K10( the carrier of T))
union F is Element of K10( the carrier of T)
X is set
X is set
x is Element of K10( the carrier of T)
Y is Element of K10(K10( the carrier of T))
union Y is Element of K10( the carrier of T)
X is set
A2 is Element of K10( the carrier of T)
B3 is Element of K10( the carrier of T)
Y3 is Element of the carrier of T
Component_of Y3 is non empty connected Element of K10( the carrier of T)
X is Element of K10( the carrier of T)
X is Element of K10( the carrier of T)
X is set
X is set
x is Element of K10( the carrier of T)
Y is set
{} T is empty proper closed connected 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 non empty set
A is Element of K10( the carrier of T)
F is Element of K10( the carrier of T)
A \ F is Element of K10( the carrier of T)
K10(K10( the carrier of T)) is non empty set
X is Element of K10(K10( the carrier of T))
union X is Element of K10( the carrier of T)
X is Element of K10(K10( the carrier of T))
union X is Element of K10( the carrier of T)
X \ X is Element of K10(K10( the carrier of T))
x is Element of K10(K10( the carrier of T))
union x is Element of K10( the carrier of T)
Y is set
X is set
A2 is Element of K10( the carrier of T)
Y3 is set
B3 is Element of K10( the carrier of T)
A2 /\ B3 is Element of K10( the carrier of T)
Y is Element of K10( the carrier of T)
Y is set
X is set
A2 is Element of K10( the carrier of T)
T is TopStruct
the carrier of T is set
K10( the carrier of T) is non empty set
F is Element of the carrier of T
A is Element of K10( the carrier of T)
T | A is strict SubSpace of T
the carrier of (T | A) is set
[#] (T | A) is non proper Element of K10( the carrier of (T | A))
K10( the carrier of (T | A)) is non empty set
T is TopStruct
the carrier of T is set
K10( the carrier of T) is non empty set
A is Element of K10( the carrier of T)
T | A is strict SubSpace of T
the carrier of (T | A) is set
F is Element of the carrier of (T | A)
T is TopStruct
the carrier of T is set
K10( the carrier of T) is non empty set
A is Element of K10( the carrier of T)
F is Element of K10( the carrier of T)
A /\ F is Element of K10( the carrier of T)
T | F is strict SubSpace of T
the carrier of (T | F) is set
K10( the carrier of (T | F)) is non empty set
[#] (T | F) is non proper Element of K10( the carrier of (T | F))
T is TopStruct
the carrier of T is set
K10( the carrier of T) is non empty set
A is Element of K10( the carrier of T)
T | A is strict SubSpace of T
the carrier of (T | A) is set
K10( the carrier of (T | A)) is non empty set
F is Element of K10( the carrier of (T | A))
T is TopStruct
the carrier of T is set
K10( the carrier of T) is non empty set
F is Element of the carrier of T
A is Element of K10( the carrier of T)
T | A is strict SubSpace of T
the carrier of (T | A) is set
[#] (T | A) is non proper Element of K10( the carrier of (T | A))
K10( the carrier of (T | A)) is non empty set
X is Element of the carrier of (T | A)
Component_of X is Element of K10( the carrier of (T | A))
X is Element of K10( the carrier of T)
x is Element of the carrier of (T | A)
Component_of x is Element of K10( the carrier of (T | A))
[#] (T | A) is non proper Element of K10( the carrier of (T | A))
K10( the carrier of (T | A)) is non empty set
X is Element of K10( the carrier of T)
x is Element of K10( the carrier of T)
X is Element of the carrier of (T | A)
Component_of X is Element of K10( the carrier of (T | A))
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
K10( the carrier of T) is non empty set
A is Element of K10( the carrier of T)
F is Element of the carrier of T
(T,A,F) is Element of K10( the carrier of T)
X is non empty Element of K10( the carrier of T)
T | X is non empty strict TopSpace-like SubSpace of T
the carrier of (T | X) is non empty set
X is Element of the carrier of (T | X)
Component_of X is non empty connected Element of K10( the carrier of (T | X))
K10( the carrier of (T | X)) is non empty set
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
K10( the carrier of T) is non empty set
A is Element of K10( the carrier of T)
T | A is strict TopSpace-like SubSpace of T
F is Element of the carrier of T
(T,A,F) is Element of K10( the carrier of T)
(T,A,F) is Element of the carrier of (T | A)
the carrier of (T | A) is set
Component_of (T,A,F) is Element of K10( the carrier of (T | A))
K10( the carrier of (T | A)) is non empty set
T is TopSpace-like TopStruct
the carrier of T is set
K10( the carrier of T) is non empty set
A is Element of K10( the carrier of T)
F is Element of K10( the carrier of T)
T | F is strict TopSpace-like SubSpace of T
(T,A,F) is Element of K10( the carrier of (T | F))
the carrier of (T | F) is set
K10( the carrier of (T | F)) is non empty set
A /\ F is Element of K10( the carrier of T)
the topology of T is non empty Element of K10(K10( the carrier of T))
K10(K10( the carrier of T)) is non empty set
[#] (T | F) is non proper closed Element of K10( the carrier of (T | F))
A /\ ([#] (T | F)) is Element of K10( the carrier of (T | F))
the topology of (T | F) is non empty Element of K10(K10( the carrier of (T | F)))
K10(K10( the carrier of (T | F))) is non empty set
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
K10( the carrier of T) is non empty set
A is Element of K10( the carrier of T)
F is Element of K10( the carrier of T)
T | F is strict TopSpace-like SubSpace of T
(T,A,F) is Element of K10( the carrier of (T | F))
the carrier of (T | F) is set
K10( the carrier of (T | F)) is non empty set
A /\ F is Element of K10( the carrier of T)
Cl (T,A,F) is Element of K10( the carrier of (T | F))
Cl A is Element of K10( the carrier of T)
(Cl A) /\ F is Element of K10( the carrier of T)
[#] (T | F) is non proper closed Element of K10( the carrier of (T | F))
(Cl A) /\ ([#] (T | F)) is Element of K10( the carrier of (T | F))
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
K10( the carrier of T) is non empty set
A is Element of K10( the carrier of T)
T | A is strict TopSpace-like SubSpace of T
the carrier of (T | A) is set
K10( the carrier of (T | A)) is non empty set
F is Element of K10( the carrier of (T | A))
Cl F is Element of K10( the carrier of (T | A))
(T,A,F) is Element of K10( the carrier of T)
Cl (T,A,F) is Element of K10( the carrier of T)
(Cl (T,A,F)) /\ A is Element of K10( the carrier of T)
[#] (T | A) is non proper closed Element of K10( the carrier of (T | A))
(T,(T,A,F),A) is Element of K10( the carrier of (T | A))
(T,A,F) /\ A is Element of K10( the carrier of T)
Cl (T,(T,A,F),A) is Element of K10( the carrier of (T | A))
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
K10( the carrier of T) is non empty set
A is Element of K10( the carrier of T)
F is Element of K10( the carrier of T)
T | F is strict TopSpace-like SubSpace of T
(T,A,F) is Element of K10( the carrier of (T | F))
the carrier of (T | F) is set
K10( the carrier of (T | F)) is non empty set
A /\ F is Element of K10( the carrier of T)
Cl (T,A,F) is Element of K10( the carrier of (T | F))
Cl A is Element of K10( the carrier of T)
(Cl A) /\ F 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 non empty set
A is Element of K10( the carrier of T)
T | A is strict TopSpace-like SubSpace of T
the carrier of (T | A) is set
K10( the carrier of (T | A)) is non empty set
F is Element of K10( the carrier of (T | A))
(T,A,F) is Element of K10( the carrier of T)
(T,(T,A,F),A) is Element of K10( the carrier of (T | A))
(T,A,F) /\ A 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 non empty set
A is Element of K10( the carrier of T)
F is Element of the carrier of T
(T,A,F) is Element of K10( the carrier of T)
X is non empty Element of K10( the carrier of T)
T | X is non empty strict TopSpace-like SubSpace of T
(T,X,F) is Element of the carrier of (T | X)
the carrier of (T | X) is non empty set
Component_of (T,X,F) is non empty connected Element of K10( the carrier of (T | X))
K10( the carrier of (T | X)) is non empty set
T | A is strict TopSpace-like SubSpace of T
(T,A,F) is Element of the carrier of (T | A)
the carrier of (T | A) is set
Component_of (T,A,F) is Element of K10( the carrier of (T | A))
K10( the carrier of (T | A)) is non empty set
T is non empty TopSpace-like TopStruct
[#] T is non empty non proper closed Element of K10( the carrier of T)
the carrier of T is non empty set
K10( the carrier of T) is non empty set
A is (T)
T is non empty TopSpace-like TopStruct
A is non empty (T)
the carrier of T is non empty set
K10( the carrier of T) is non empty set
K10(K10( the carrier of T)) is non empty set
F is Element of K10(K10( the carrier of T))
union F is Element of K10( the carrier of T)
X is set
X is Element of K10( the carrier of T)
{X} is set
x is set
Y is Element of K10( the carrier of T)
x is set