K87() is set
K10(K87()) is set
K179() is non empty strict TopSpace-like TopStruct
the carrier of K179() is non empty set
{} is empty set
1 is non empty set
X is non empty TopSpace-like TopStruct
the carrier of X is non empty set
K10( the carrier of X) is set
X0 is Element of K10( the carrier of X)
D is Element of K10( the carrier of X)
X0 ` is Element of K10( the carrier of X)
D ` is Element of K10( the carrier of X)
X is non empty TopSpace-like TopStruct
the carrier of X is non empty set
K10( the carrier of X) is set
X0 is Element of K10( the carrier of X)
D is Element of K10( the carrier of X)
X0 /\ D is Element of K10( the carrier of X)
X is non empty TopSpace-like TopStruct
the carrier of X is non empty set
K10( the carrier of X) is set
X0 is Element of K10( the carrier of X)
D is Element of K10( the carrier of X)
X0 /\ D is Element of K10( the carrier of X)
X is non empty TopSpace-like TopStruct
the carrier of X is non empty set
K10( the carrier of X) is set
X0 is Element of K10( the carrier of X)
D is Element of K10( the carrier of X)
X0 ` is Element of K10( the carrier of X)
D ` is Element of K10( the carrier of X)
X is non empty TopSpace-like TopStruct
the carrier of X is non empty set
K10( the carrier of X) is set
X0 is Element of K10( the carrier of X)
D is Element of K10( the carrier of X)
X is non empty TopSpace-like TopStruct
the carrier of X is non empty set
K10( the carrier of X) is set
X0 is Element of K10( the carrier of X)
D is Element of K10( the carrier of X)
X0 ` is Element of K10( the carrier of X)
D ` is Element of K10( the carrier of X)
X is non empty TopSpace-like TopStruct
the carrier of X is non empty set
K10( the carrier of X) is set
X0 is Element of K10( the carrier of X)
D is Element of K10( the carrier of X)
X is non empty TopSpace-like TopStruct
X0 is non empty TopSpace-like SubSpace of X
D is non empty TopSpace-like SubSpace of X
the carrier of X is non empty set
K10( the carrier of X) is set
the carrier of X0 is non empty set
the carrier of D is non empty set
C is Element of K10( the carrier of X)
B is Element of K10( the carrier of X)
X is non empty non trivial TopSpace-like TopStruct
the carrier of X is non empty non trivial set
K10( the carrier of X) is set
X0 is non empty proper Element of K10( the carrier of X)
D is non empty strict TopSpace-like SubSpace of X
the carrier of D is non empty set
C is non empty strict TopSpace-like proper SubSpace of X
the carrier of C is non empty set
X is non empty non trivial TopSpace-like TopStruct
X0 is non empty TopSpace-like proper SubSpace of X
the carrier of X is non empty non trivial set
K10( the carrier of X) is set
the carrier of X0 is non empty set
D is Element of K10( the carrier of X)
D ` is Element of K10( the carrier of X)
C is non empty strict TopSpace-like SubSpace of X
the carrier of C is non empty set
B is Element of K10( the carrier of X)
X1 is Element of K10( the carrier of X)
B is non empty strict TopSpace-like proper SubSpace of X
X is non empty TopSpace-like TopStruct
X is non empty TopSpace-like TopStruct
the carrier of X is non empty set
K10( the carrier of X) is set
X0 is TopSpace-like SubSpace of X
the carrier of X0 is set
D is Element of K10( the carrier of X)
C is Element of K10( the carrier of X)
X is non empty TopSpace-like TopStruct
X0 is TopSpace-like SubSpace of X
the carrier of X is non empty set
K10( the carrier of X) is set
the carrier of X0 is set
D is Element of K10( the carrier of X)
Cl D is closed Element of K10( the carrier of X)
X0 is TopSpace-like SubSpace of X
X0 is TopSpace-like SubSpace of X
X is non empty TopSpace-like TopStruct
the carrier of X is non empty set
K10( the carrier of X) is set
X0 is Element of K10( the carrier of X)
D is non empty strict TopSpace-like SubSpace of X
the carrier of D is non empty set
C is Element of K10( the carrier of X)
[#] X is non empty non proper open closed dense non boundary Element of K10( the carrier of X)
X is non empty TopSpace-like TopStruct
the carrier of X is non empty set
K10( the carrier of X) is set
X0 is non empty Element of K10( the carrier of X)
D is non empty strict TopSpace-like SubSpace of X
the carrier of D is non empty set
C is non empty strict TopSpace-like (X) SubSpace of X
the carrier of C is non empty set
X is non empty TopSpace-like TopStruct
the carrier of X is non empty set
K10( the carrier of X) is set
X0 is non empty TopSpace-like (X) SubSpace of X
the carrier of X0 is non empty set
K10( the carrier of X0) is set
D is Element of K10( the carrier of X)
C is Element of K10( the carrier of X0)
B is Element of K10( the carrier of X)
X is non empty TopSpace-like TopStruct
X0 is TopSpace-like (X) SubSpace of X
D is TopSpace-like SubSpace of X
the carrier of X is non empty set
K10( the carrier of X) is set
the carrier of X0 is set
the carrier of D is set
C is Element of K10( the carrier of X)
B is Element of K10( the carrier of X)
X is non empty TopSpace-like TopStruct
X0 is non empty TopSpace-like (X) SubSpace of X
D is non empty TopSpace-like SubSpace of X
the carrier of X is non empty set
K10( the carrier of X) is set
the carrier of X0 is non empty set
C is Element of K10( the carrier of X)
the carrier of D is non empty set
K10( the carrier of D) is set
B is Element of K10( the carrier of D)
X is non empty TopSpace-like TopStruct
X0 is non empty TopSpace-like (X) SubSpace of X
D is non empty TopSpace-like (X0) SubSpace of X0
the carrier of X is non empty set
K10( the carrier of X) is set
the carrier of X0 is non empty set
B is Element of K10( the carrier of X)
the carrier of D is non empty set
K10( the carrier of X0) is set
C is Element of K10( the carrier of X)
X1 is Element of K10( the carrier of X0)
X is non empty TopSpace-like TopStruct
D is non empty TopSpace-like TopStruct
X0 is non empty TopSpace-like TopStruct
the carrier of X0 is non empty set
the topology of X0 is non empty Element of K10(K10( the carrier of X0))
K10( the carrier of X0) is set
K10(K10( the carrier of X0)) is set
TopStruct(# the carrier of X0, the topology of X0 #) is non empty strict TopSpace-like TopStruct
the carrier of X is non empty set
K10( the carrier of X) is set
C is TopSpace-like SubSpace of X
the carrier of C is set
B is Element of K10( the carrier of X)
the carrier of X is non empty set
K10( the carrier of X) is set
C is TopSpace-like SubSpace of X
the carrier of C is set
B is Element of K10( the carrier of X)
X is non empty TopSpace-like TopStruct
X is non empty TopSpace-like TopStruct
the carrier of X is non empty set
K10( the carrier of X) is set
X0 is TopSpace-like SubSpace of X
the carrier of X0 is set
D is Element of K10( the carrier of X)
C is Element of K10( the carrier of X)
X is non empty TopSpace-like TopStruct
X0 is TopSpace-like SubSpace of X
the carrier of X is non empty set
K10( the carrier of X) is set
D is Element of K10( the carrier of X)
the carrier of X0 is set
X0 is TopSpace-like SubSpace of X
X0 is TopSpace-like SubSpace of X
the carrier of X is non empty set
K10( the carrier of X) is set
D is Element of K10( the carrier of X)
the carrier of X0 is set
[#] X is non empty non proper open closed dense non boundary Element of K10( the carrier of X)
X0 is TopSpace-like SubSpace of X
X is non empty TopSpace-like TopStruct
the carrier of X is non empty set
K10( the carrier of X) is set
X0 is Element of K10( the carrier of X)
D is non empty strict TopSpace-like SubSpace of X
the carrier of D is non empty set
C is Element of K10( the carrier of X)
[#] X is non empty non proper open closed dense non boundary Element of K10( the carrier of X)
X is non empty TopSpace-like TopStruct
the carrier of X is non empty set
K10( the carrier of X) is set
X0 is non empty Element of K10( the carrier of X)
D is non empty strict TopSpace-like SubSpace of X
the carrier of D is non empty set
C is non empty strict TopSpace-like (X) (X) SubSpace of X
the carrier of C is non empty set
X is non empty TopSpace-like TopStruct
the carrier of X is non empty set
K10( the carrier of X) is set
X0 is non empty TopSpace-like (X) (X) SubSpace of X
the carrier of X0 is non empty set
K10( the carrier of X0) is set
D is Element of K10( the carrier of X)
C is Element of K10( the carrier of X0)
B is Element of K10( the carrier of X)
X is non empty TopSpace-like TopStruct
X0 is TopSpace-like (X) (X) SubSpace of X
D is TopSpace-like SubSpace of X
the carrier of X is non empty set
K10( the carrier of X) is set
the carrier of X0 is set
the carrier of D is set
C is Element of K10( the carrier of X)
B is Element of K10( the carrier of X)
X is non empty TopSpace-like TopStruct
X0 is non empty TopSpace-like (X) (X) SubSpace of X
D is non empty TopSpace-like SubSpace of X
the carrier of X is non empty set
K10( the carrier of X) is set
the carrier of X0 is non empty set
C is Element of K10( the carrier of X)
the carrier of D is non empty set
K10( the carrier of D) is set
B is Element of K10( the carrier of D)
X is non empty TopSpace-like TopStruct
X0 is non empty TopSpace-like (X) (X) SubSpace of X
D is non empty TopSpace-like (X0) (X0) SubSpace of X0
the carrier of X is non empty set
K10( the carrier of X) is set
the carrier of X0 is non empty set
B is Element of K10( the carrier of X)
the carrier of D is non empty set
K10( the carrier of X0) is set
C is Element of K10( the carrier of X)
X1 is Element of K10( the carrier of X0)
X is non empty TopSpace-like TopStruct
D is non empty TopSpace-like TopStruct
X0 is non empty TopSpace-like TopStruct
the carrier of X0 is non empty set
the topology of X0 is non empty Element of K10(K10( the carrier of X0))
K10( the carrier of X0) is set
K10(K10( the carrier of X0)) is set
TopStruct(# the carrier of X0, the topology of X0 #) is non empty strict TopSpace-like TopStruct
the carrier of X is non empty set
K10( the carrier of X) is set
C is TopSpace-like SubSpace of X
the carrier of C is set
B is Element of K10( the carrier of X)
the carrier of X is non empty set
K10( the carrier of X) is set
C is TopSpace-like SubSpace of X
the carrier of C is set
B is Element of K10( the carrier of X)
X is non empty TopSpace-like TopStruct
X0 is TopSpace-like SubSpace of X
the carrier of X is non empty set
K10( the carrier of X) is set
D is Element of K10( the carrier of X)
the carrier of X0 is set
X0 is TopSpace-like SubSpace of X
X0 is TopSpace-like SubSpace of X
X is non empty TopSpace-like TopStruct
the carrier of X is non empty set
K10( the carrier of X) is set
X0 is Element of K10( the carrier of X)
[#] X is non empty non proper open closed dense non boundary Element of K10( the carrier of X)
D is non empty strict TopSpace-like (X) SubSpace of X
the carrier of D is non empty set
C is Element of K10( the carrier of X)
X is non empty TopSpace-like TopStruct
the carrier of X is non empty set
K10( the carrier of X) is set
X0 is non empty Element of K10( the carrier of X)
D is non empty strict TopSpace-like SubSpace of X
the carrier of D is non empty set
C is non empty strict TopSpace-like open (X) (X) SubSpace of X
the carrier of C is non empty set
X is non empty TopSpace-like TopStruct
X0 is TopSpace-like SubSpace of X
the carrier of X is non empty set
K10( the carrier of X) is set
the carrier of X0 is set
D is Element of K10( the carrier of X)
C is Element of K10( the carrier of X)
B is non empty strict TopSpace-like open (X) (X) SubSpace of X
the carrier of B is non empty set
C is strict TopSpace-like open (X) (X) SubSpace of X
the carrier of C is set
B is Element of K10( the carrier of X)
X1 is Element of K10( the carrier of X)
D is Element of K10( the carrier of X)
X1 is Element of K10( the carrier of X)
X2 is Element of K10( the carrier of X)
X is non empty TopSpace-like TopStruct
X0 is non empty TopSpace-like SubSpace of X
D is non empty TopSpace-like SubSpace of X
X0 union D is non empty strict TopSpace-like SubSpace of X
the carrier of X is non empty set
K10( the carrier of X) is set
the carrier of X0 is non empty set
the carrier of D is non empty set
the carrier of (X0 union D) is non empty set
C is Element of K10( the carrier of X)
B is Element of K10( the carrier of X)
C \/ B is Element of K10( the carrier of X)
X1 is Element of K10( the carrier of X)
X is non empty TopSpace-like TopStruct
X0 is non empty TopSpace-like SubSpace of X
D is non empty TopSpace-like SubSpace of X
X0 union D is non empty strict TopSpace-like SubSpace of X
the carrier of X is non empty set
K10( the carrier of X) is set
the carrier of X0 is non empty set
the carrier of D is non empty set
the carrier of (X0 union D) is non empty set
C is Element of K10( the carrier of X)
B is Element of K10( the carrier of X)
C \/ B is Element of K10( the carrier of X)
X1 is Element of K10( the carrier of X)
X is non empty TopSpace-like TopStruct
X0 is non empty TopSpace-like SubSpace of X
D is non empty TopSpace-like SubSpace of X
X0 meet D is non empty strict TopSpace-like SubSpace of X
the carrier of X is non empty set
K10( the carrier of X) is set
the carrier of X0 is non empty set
the carrier of D is non empty set
the carrier of (X0 meet D) is non empty set
C is Element of K10( the carrier of X)
B is Element of K10( the carrier of X)
C /\ B is Element of K10( the carrier of X)
X1 is Element of K10( the carrier of X)
X is non empty TopSpace-like TopStruct
X0 is non empty TopSpace-like SubSpace of X
D is non empty TopSpace-like SubSpace of X
X0 meet D is non empty strict TopSpace-like SubSpace of X
the carrier of X is non empty set
K10( the carrier of X) is set
the carrier of X0 is non empty set
the carrier of D is non empty set
the carrier of (X0 meet D) is non empty set
C is Element of K10( the carrier of X)
B is Element of K10( the carrier of X)
C /\ B is Element of K10( the carrier of X)
X1 is Element of K10( the carrier of X)
X is non empty TopSpace-like TopStruct
X is non empty TopSpace-like TopStruct
the carrier of X is non empty set
K10( the carrier of X) is set
X0 is TopSpace-like SubSpace of X
the carrier of X0 is set
D is Element of K10( the carrier of X)
C is Element of K10( the carrier of X)
X is non empty TopSpace-like TopStruct
X0 is non empty TopSpace-like SubSpace of X
the carrier of X is non empty set
K10( the carrier of X) is set
the carrier of X0 is non empty set
D is Element of K10( the carrier of X)
Int D is open Element of K10( the carrier of X)
X0 is non empty TopSpace-like SubSpace of X
X0 is TopSpace-like SubSpace of X
the carrier of X is non empty set
K10( the carrier of X) is set
the carrier of X0 is set
D is Element of K10( the carrier of X)
X0 is TopSpace-like SubSpace of X
X is non empty TopSpace-like TopStruct
the carrier of X is non empty set
K10( the carrier of X) is set
X0 is non empty Element of K10( the carrier of X)
D is non empty strict TopSpace-like SubSpace of X
the carrier of D is non empty set
X is non empty TopSpace-like TopStruct
X0 is TopSpace-like SubSpace of X
D is TopSpace-like SubSpace of X
the carrier of X is non empty set
K10( the carrier of X) is set
the carrier of X0 is set
the carrier of D is set
X1 is Element of K10( the carrier of X)
C is Element of K10( the carrier of X)
X1 is Element of K10( the carrier of X)
B is Element of K10( the carrier of X)
X is non empty TopSpace-like TopStruct
X0 is non empty TopSpace-like SubSpace of X
D is non empty TopSpace-like SubSpace of X
X is non empty TopSpace-like TopStruct
the carrier of X is non empty set
K10( the carrier of X) is set
X0 is TopSpace-like SubSpace of X
the carrier of X0 is set
D is Element of K10( the carrier of X)
C is Element of K10( the carrier of X)
X is non empty TopSpace-like TopStruct
X0 is TopSpace-like SubSpace of X
D is TopSpace-like SubSpace of X
the carrier of D is set
the carrier of X0 is set
the carrier of X is non empty set
K10( the carrier of X) is set
C is Element of K10( the carrier of X)
X is non empty TopSpace-like TopStruct
X is non empty TopSpace-like TopStruct
the carrier of X is non empty set
K10( the carrier of X) is set
X0 is TopSpace-like SubSpace of X
the carrier of X0 is set
D is Element of K10( the carrier of X)
C is Element of K10( the carrier of X)
X is non empty TopSpace-like TopStruct
X0 is TopSpace-like SubSpace of X
the carrier of X is non empty set
K10( the carrier of X) is set
D is Element of K10( the carrier of X)
the carrier of X0 is set
X0 is TopSpace-like SubSpace of X
X0 is TopSpace-like SubSpace of X
the carrier of X is non empty set
K10( the carrier of X) is set
the carrier of X0 is set
D is Element of K10( the carrier of X)
X0 is TopSpace-like SubSpace of X
X is non empty TopSpace-like TopStruct
the carrier of X is non empty set
K10( the carrier of X) is set
X0 is non empty Element of K10( the carrier of X)
D is non empty strict TopSpace-like SubSpace of X
the carrier of D is non empty set
X is non empty TopSpace-like TopStruct
X0 is TopSpace-like SubSpace of X
D is TopSpace-like SubSpace of X
the carrier of X is non empty set
K10( the carrier of X) is set
the carrier of X0 is set
the carrier of D is set
X1 is Element of K10( the carrier of X)
C is Element of K10( the carrier of X)
X1 is Element of K10( the carrier of X)
B is Element of K10( the carrier of X)
X is non empty TopSpace-like TopStruct
X0 is non empty TopSpace-like SubSpace of X
D is non empty TopSpace-like SubSpace of X
X is non empty TopSpace-like TopStruct
the carrier of X is non empty set
K10( the carrier of X) is set
X0 is TopSpace-like SubSpace of X
the carrier of X0 is set
D is Element of K10( the carrier of X)
C is Element of K10( the carrier of X)
X is non empty TopSpace-like TopStruct
X0 is TopSpace-like SubSpace of X
D is TopSpace-like SubSpace of X
the carrier of D is set
the carrier of X0 is set
the carrier of X is non empty set
K10( the carrier of X) is set
C is Element of K10( the carrier of X)
X is non empty TopSpace-like TopStruct
X0 is TopSpace-like SubSpace of X
the carrier of X is non empty set
K10( the carrier of X) is set
D is Element of K10( the carrier of X)
the carrier of X0 is set
X0 is TopSpace-like SubSpace of X
X0 is TopSpace-like SubSpace of X
X is non empty TopSpace-like TopStruct
the carrier of X is non empty set
K10( the carrier of X) is set
X0 is non empty Element of K10( the carrier of X)
D is non empty strict TopSpace-like SubSpace of X
the carrier of D is non empty set
C is non empty strict TopSpace-like closed SubSpace of X
the carrier of C is non empty set
X is non empty TopSpace-like TopStruct
X0 is non empty TopSpace-like SubSpace of X
the carrier of X is non empty set
K10( the carrier of X) is set
the carrier of X0 is non empty set
D is Element of K10( the carrier of X)
C is Element of K10( the carrier of X)
B is non empty strict TopSpace-like closed SubSpace of X
the carrier of B is non empty set
C is non empty strict TopSpace-like closed SubSpace of X
the carrier of C is non empty set
B is Element of K10( the carrier of X)
D is Element of K10( the carrier of X)
X1 is Element of K10( the carrier of X)
X1 is Element of K10( the carrier of X)
X2 is Element of K10( the carrier of X)
X is non empty TopSpace-like TopStruct
X0 is non empty TopSpace-like SubSpace of X
D is non empty TopSpace-like SubSpace of X
X0 meet D is non empty strict TopSpace-like SubSpace of X
X is non empty TopSpace-like TopStruct
X0 is non empty TopSpace-like SubSpace of X
D is non empty TopSpace-like SubSpace of X
X0 union D is non empty strict TopSpace-like SubSpace of X
the carrier of X is non empty set
K10( the carrier of X) is set
the carrier of X0 is non empty set
the carrier of D is non empty set
C is Element of K10( the carrier of X)
B is Element of K10( the carrier of X)
C \/ B is Element of K10( the carrier of X)
the carrier of (X0 union D) is non empty set
X1 is Element of K10( the carrier of X)
X is non empty TopSpace-like TopStruct
X0 is non empty TopSpace-like SubSpace of X
D is non empty TopSpace-like SubSpace of X
X0 union D is non empty strict TopSpace-like SubSpace of X
the carrier of X is non empty set
K10( the carrier of X) is set
the carrier of X0 is non empty set
the carrier of D is non empty set
C is Element of K10( the carrier of X)
B is Element of K10( the carrier of X)
C \/ B is Element of K10( the carrier of X)
the carrier of (X0 union D) is non empty set
X1 is Element of K10( the carrier of X)
X is non empty TopSpace-like TopStruct
X0 is non empty TopSpace-like SubSpace of X
D is non empty TopSpace-like SubSpace of X
X0 meet D is non empty strict TopSpace-like SubSpace of X
X is non empty TopSpace-like TopStruct
the carrier of X is non empty set
K10( the carrier of X) is set
X0 is non empty Element of K10( the carrier of X)
D is non empty strict TopSpace-like SubSpace of X
the carrier of D is non empty set
X is non empty non trivial TopSpace-like TopStruct
the carrier of X is non empty non trivial set
K10( the carrier of X) is set
X0 is Element of K10( the carrier of X)
D is non empty strict TopSpace-like SubSpace of X
the carrier of D is non empty set
C is strict TopSpace-like proper SubSpace of X
X is non empty TopSpace-like discrete almost_discrete extremally_disconnected hereditarily_extremally_disconnected TopStruct
X0 is non empty TopSpace-like closed open discrete almost_discrete extremally_disconnected hereditarily_extremally_disconnected (X) (X) SubSpace of X
X0 is TopSpace-like closed open discrete almost_discrete SubSpace of X
X0 is TopSpace-like closed open discrete almost_discrete SubSpace of X
X is non empty TopSpace-like discrete almost_discrete extremally_disconnected hereditarily_extremally_disconnected TopStruct
the non empty strict TopSpace-like closed open discrete almost_discrete extremally_disconnected hereditarily_extremally_disconnected (X) (X) SubSpace of X is non empty strict TopSpace-like closed open discrete almost_discrete extremally_disconnected hereditarily_extremally_disconnected (X) (X) SubSpace of X
X is non empty non trivial TopSpace-like discrete almost_discrete extremally_disconnected hereditarily_extremally_disconnected TopStruct
the strict TopSpace-like closed open discrete almost_discrete proper V96(X) (X) (X) SubSpace of X is strict TopSpace-like closed open discrete almost_discrete proper V96(X) (X) (X) SubSpace of X
X is non empty TopSpace-like TopStruct
X0 is non empty TopSpace-like SubSpace of X
X is non empty TopSpace-like TopStruct
X0 is non empty TopSpace-like SubSpace of X
X is non empty non trivial TopSpace-like non discrete TopStruct
the carrier of X is non empty non trivial set
K10( the carrier of X) is set
X0 is non empty Element of K10( the carrier of X)
D is non empty strict TopSpace-like SubSpace of X
the carrier of D is non empty set
C is Element of K10( the carrier of X)
the carrier of X is non empty non trivial set
K10( the carrier of X) is set
X0 is Element of K10( the carrier of X)
D is non empty strict TopSpace-like (X) (X) SubSpace of X
the carrier of D is non empty set
X is non empty non trivial TopSpace-like non discrete TopStruct
the carrier of X is non empty non trivial set
K10( the carrier of X) is set
X0 is non empty Element of K10( the carrier of X)
D is strict TopSpace-like SubSpace of X
the carrier of D is set
X is non empty non trivial TopSpace-like non discrete TopStruct
the carrier of X is non empty non trivial set
K10( the carrier of X) is set
X0 is non empty proper Element of K10( the carrier of X)
D is non empty strict TopSpace-like SubSpace of X
the carrier of D is non empty set
C is strict TopSpace-like non closed proper (X) (X) SubSpace of X
the carrier of C is set
X is non empty non trivial TopSpace-like non discrete TopStruct
X0 is non empty TopSpace-like non open proper (X) (X) SubSpace of X
D is non empty strict TopSpace-like proper SubSpace of X
C is non empty strict TopSpace-like non closed proper (X) (X) SubSpace of X
X is non empty non trivial TopSpace-like non discrete TopStruct
X0 is non empty TopSpace-like non closed proper (X) (X) SubSpace of X
D is non empty strict TopSpace-like proper SubSpace of X
C is non empty strict TopSpace-like non open proper (X) (X) SubSpace of X
X is non empty non trivial TopSpace-like non discrete TopStruct
D is non empty TopSpace-like TopStruct
X0 is non empty TopSpace-like TopStruct
the carrier of X0 is non empty set
the topology of X0 is non empty Element of K10(K10( the carrier of X0))
K10( the carrier of X0) is set
K10(K10( the carrier of X0)) is set
TopStruct(# the carrier of X0, the topology of X0 #) is non empty strict TopSpace-like TopStruct
the carrier of X is non empty non trivial set
K10( the carrier of X) is set
C is TopSpace-like SubSpace of X
the carrier of C is set
B is Element of K10( the carrier of X)
the carrier of X is non empty non trivial set
K10( the carrier of X) is set
C is TopSpace-like SubSpace of X
the carrier of C is set
B is Element of K10( the carrier of X)
X is non empty TopSpace-like TopStruct
the carrier of X is non empty set
K10( the carrier of X) is set
X0 is non empty Element of K10( the carrier of X)
D is non empty strict TopSpace-like SubSpace of X
the carrier of D is non empty set
X is non empty non trivial TopSpace-like TopStruct
the carrier of X is non empty non trivial set
K10( the carrier of X) is set
X0 is Element of K10( the carrier of X)
D is non empty strict TopSpace-like SubSpace of X
the carrier of D is non empty set
C is strict TopSpace-like proper SubSpace of X
X is non empty TopSpace-like almost_discrete extremally_disconnected hereditarily_extremally_disconnected TopStruct
X0 is non empty TopSpace-like almost_discrete extremally_disconnected hereditarily_extremally_disconnected SubSpace of X
the carrier of X is non empty set
K10( the carrier of X) is set
the carrier of X0 is non empty set
D is Element of K10( the carrier of X)
X0 is TopSpace-like SubSpace of X
the carrier of X is non empty set
K10( the carrier of X) is set
the carrier of X0 is set
D is Element of K10( the carrier of X)
X0 is TopSpace-like SubSpace of X
X0 is non empty TopSpace-like almost_discrete extremally_disconnected hereditarily_extremally_disconnected (X) SubSpace of X
X0 is non empty TopSpace-like almost_discrete extremally_disconnected hereditarily_extremally_disconnected (X) SubSpace of X
X0 is TopSpace-like SubSpace of X
X0 is TopSpace-like SubSpace of X
X0 is TopSpace-like SubSpace of X
X is non empty TopSpace-like almost_discrete extremally_disconnected hereditarily_extremally_disconnected TopStruct
the non empty strict TopSpace-like almost_discrete extremally_disconnected hereditarily_extremally_disconnected (X) SubSpace of X is non empty strict TopSpace-like almost_discrete extremally_disconnected hereditarily_extremally_disconnected (X) SubSpace of X
X is non empty non trivial TopSpace-like almost_discrete extremally_disconnected hereditarily_extremally_disconnected TopStruct
the strict TopSpace-like proper (X) SubSpace of X is strict TopSpace-like proper (X) SubSpace of X
X is non empty TopSpace-like TopStruct
X0 is non empty TopSpace-like SubSpace of X
X is non empty TopSpace-like TopStruct
X0 is non empty TopSpace-like SubSpace of X
X is non empty TopSpace-like TopStruct
X0 is non empty TopSpace-like SubSpace of X
X is non empty TopSpace-like TopStruct
X0 is non empty TopSpace-like SubSpace of X
X is non empty non trivial TopSpace-like non discrete non anti-discrete non almost_discrete TopStruct
the carrier of X is non empty non trivial set
K10( the carrier of X) is set
X0 is non empty Element of K10( the carrier of X)
D is non empty strict TopSpace-like SubSpace of X
the carrier of D is non empty set
C is Element of K10( the carrier of X)
the carrier of X is non empty non trivial set
K10( the carrier of X) is set
X0 is Element of K10( the carrier of X)
D is non empty strict TopSpace-like (X) (X) (X) (X) SubSpace of X
the carrier of D is non empty set
X is non empty non trivial TopSpace-like non discrete non anti-discrete non almost_discrete TopStruct
the carrier of X is non empty non trivial set
K10( the carrier of X) is set
X0 is non empty Element of K10( the carrier of X)
D is non empty strict TopSpace-like SubSpace of X
the carrier of D is non empty set
C is non empty strict TopSpace-like non open proper (X) (X) (X) (X) SubSpace of X
the carrier of C is non empty set
X is non empty non trivial TopSpace-like non discrete non anti-discrete non almost_discrete TopStruct
the carrier of X is non empty non trivial set
K10( the carrier of X) is set
X0 is non empty proper Element of K10( the carrier of X)
D is non empty strict TopSpace-like (X) (X) (X) (X) SubSpace of X
the carrier of D is non empty set
C is strict TopSpace-like non closed proper (X) (X) (X) (X) SubSpace of X
the carrier of C is set
X is non empty non trivial TopSpace-like non discrete non anti-discrete non almost_discrete TopStruct
X0 is non empty TopSpace-like non open proper (X) (X) (X) (X) SubSpace of X
D is non empty strict TopSpace-like proper SubSpace of X
C is non empty strict TopSpace-like non closed proper (X) (X) (X) (X) SubSpace of X
X is non empty non trivial TopSpace-like non discrete non anti-discrete non almost_discrete TopStruct
X0 is non empty TopSpace-like non closed proper (X) (X) (X) (X) SubSpace of X
D is non empty strict TopSpace-like proper SubSpace of X
C is non empty strict TopSpace-like non open proper (X) (X) (X) (X) SubSpace of X
X is non empty non trivial TopSpace-like non discrete non anti-discrete non almost_discrete TopStruct
D is non empty TopSpace-like TopStruct
X0 is non empty TopSpace-like TopStruct
the carrier of X0 is non empty set
the topology of X0 is non empty Element of K10(K10( the carrier of X0))
K10( the carrier of X0) is set
K10(K10( the carrier of X0)) is set
TopStruct(# the carrier of X0, the topology of X0 #) is non empty strict TopSpace-like TopStruct
the carrier of X is non empty non trivial set
K10( the carrier of X) is set
C is TopSpace-like SubSpace of X
the carrier of C is set
B is Element of K10( the carrier of X)
the carrier of X is non empty non trivial set
K10( the carrier of X) is set
C is TopSpace-like SubSpace of X
the carrier of C is set
B is Element of K10( the carrier of X)
X is non empty non trivial TopSpace-like non discrete non anti-discrete non almost_discrete TopStruct
the carrier of X is non empty non trivial set
K10( the carrier of X) is set
X0 is non empty Element of K10( the carrier of X)
D is Element of K10( the carrier of X)
C is non empty strict TopSpace-like SubSpace of X
the carrier of C is non empty set
B is Element of K10( the carrier of X)
X1 is Element of K10( the carrier of X)
the carrier of X is non empty non trivial set
K10( the carrier of X) is set
X0 is Element of K10( the carrier of X)
D is non empty strict TopSpace-like open (X) (X) (X) (X) SubSpace of X
the carrier of D is non empty set
X is non empty non trivial TopSpace-like non discrete non anti-discrete non almost_discrete TopStruct
the carrier of X is non empty non trivial set
K10( the carrier of X) is set
X0 is non empty Element of K10( the carrier of X)
D is non empty strict TopSpace-like SubSpace of X
the carrier of D is non empty set
C is non empty strict TopSpace-like closed non open proper (X) (X) (X) (X) SubSpace of X
the carrier of C is non empty set
X is non empty non trivial TopSpace-like non discrete non anti-discrete non almost_discrete TopStruct
the carrier of X is non empty non trivial set
K10( the carrier of X) is set
X0 is non empty proper Element of K10( the carrier of X)
D is non empty strict TopSpace-like open (X) (X) (X) (X) SubSpace of X
the carrier of D is non empty set
C is strict TopSpace-like non closed open proper (X) (X) (X) (X) SubSpace of X
the carrier of C is set
X is non empty non trivial TopSpace-like non discrete non anti-discrete non almost_discrete TopStruct
X0 is non empty TopSpace-like closed non open proper (X) (X) (X) (X) SubSpace of X
D is non empty strict TopSpace-like proper SubSpace of X
C is non empty strict TopSpace-like non closed open proper (X) (X) (X) (X) SubSpace of X
X is non empty non trivial TopSpace-like non discrete non anti-discrete non almost_discrete TopStruct
X0 is non empty TopSpace-like non closed open proper (X) (X) (X) (X) SubSpace of X
D is non empty strict TopSpace-like proper SubSpace of X
C is non empty strict TopSpace-like closed non open proper (X) (X) (X) (X) SubSpace of X
X is non empty non trivial TopSpace-like non discrete non anti-discrete non almost_discrete TopStruct
X0 is non empty TopSpace-like SubSpace of X
the carrier of X is non empty non trivial set
K10( the carrier of X) is set
the carrier of X0 is non empty set
D is Element of K10( the carrier of X)
C is Element of K10( the carrier of X)
B is non empty strict TopSpace-like closed non open proper (X) (X) (X) (X) SubSpace of X
the carrier of B is non empty set
C is non empty strict TopSpace-like closed non open proper (X) (X) (X) (X) SubSpace of X
the carrier of C is non empty set
B is Element of K10( the carrier of X)
D is Element of K10( the carrier of X)
X1 is Element of K10( the carrier of X)
X1 is Element of K10( the carrier of X)
X2 is Element of K10( the carrier of X)
X is non empty non trivial TopSpace-like non discrete non anti-discrete non almost_discrete TopStruct
the carrier of X is non empty non trivial set
the topology of X is non empty Element of K10(K10( the carrier of X))
K10( the carrier of X) is set
K10(K10( the carrier of X)) is set
TopStruct(# the carrier of X, the topology of X #) is non empty strict TopSpace-like TopStruct
X0 is non empty TopSpace-like non open proper (X) (X) (X) (X) SubSpace of X
the carrier of X0 is non empty set
the topology of X0 is non empty Element of K10(K10( the carrier of X0))
K10( the carrier of X0) is set
K10(K10( the carrier of X0)) is set
TopStruct(# the carrier of X0, the topology of X0 #) is non empty strict TopSpace-like TopStruct
D is non empty Element of K10( the carrier of X)
C is Element of K10( the carrier of X)
B is Element of K10( the carrier of X)
C /\ B is Element of K10( the carrier of X)
C \/ B is Element of K10( the carrier of X)
X1 is non empty strict TopSpace-like (X) (X) (X) (X) SubSpace of X
the carrier of X1 is non empty set
X1 is non empty strict TopSpace-like closed non open proper (X) (X) (X) (X) SubSpace of X
the carrier of X1 is non empty set
X2 is non empty strict TopSpace-like non closed proper (X) (X) (X) (X) SubSpace of X
X2 meet X1 is non empty strict TopSpace-like SubSpace of X
X2 union X1 is non empty strict TopSpace-like SubSpace of X
the carrier of (X2 meet X1) is non empty set
the carrier of (X2 union X1) is non empty set
X is non empty non trivial TopSpace-like non discrete non anti-discrete non almost_discrete TopStruct
X0 is non empty TopSpace-like (X) (X) (X) (X) SubSpace of X
the carrier of X0 is non empty set
the topology of X0 is non empty Element of K10(K10( the carrier of X0))
K10( the carrier of X0) is set
K10(K10( the carrier of X0)) is set
TopStruct(# the carrier of X0, the topology of X0 #) is non empty strict TopSpace-like TopStruct
the carrier of X is non empty non trivial set
K10( the carrier of X) is set
D is non empty Element of K10( the carrier of X)
C is Element of K10( the carrier of X)
B is Element of K10( the carrier of X)
C \/ B is Element of K10( the carrier of X)
X1 is non empty strict TopSpace-like open (X) (X) (X) (X) SubSpace of X
the carrier of X1 is non empty set
[#] X is non empty non trivial non proper open closed dense non boundary Element of K10( the carrier of X)
X1 is non empty strict TopSpace-like non open proper (X) (X) (X) (X) SubSpace of X
the carrier of X1 is non empty set
X2 is non empty strict TopSpace-like non closed open proper (X) (X) (X) (X) SubSpace of X
X2 union X1 is non empty strict TopSpace-like SubSpace of X
the carrier of (X2 union X1) is non empty set
X is non empty non trivial TopSpace-like non discrete non anti-discrete non almost_discrete TopStruct
X0 is non empty TopSpace-like non open proper (X) (X) (X) (X) SubSpace of X
the carrier of X is non empty non trivial set
K10( the carrier of X) is set
the carrier of X0 is non empty set
D is non empty Element of K10( the carrier of X)
C is Element of K10( the carrier of X)
B is Element of K10( the carrier of X)
D \/ B is non empty Element of K10( the carrier of X)
C /\ (D \/ B) is Element of K10( the carrier of X)
C \/ B is Element of K10( the carrier of X)
X1 is non empty strict TopSpace-like open (X) (X) (X) (X) SubSpace of X
the carrier of X1 is non empty set
X2 is non empty strict TopSpace-like closed non open proper (X) (X) (X) (X) SubSpace of X
the carrier of X2 is non empty set
C /\ B is Element of K10( the carrier of X)
X1 is non empty strict TopSpace-like non closed open proper (X) (X) (X) (X) SubSpace of X
the carrier of X1 is non empty set
c9 is Element of K10( the carrier of X)
c10 is Element of K10( the carrier of X)
X is non empty non trivial TopSpace-like non discrete non anti-discrete non almost_discrete TopStruct
X0 is TopSpace-like non closed proper (X) (X) (X) (X) SubSpace of X
the carrier of X is non empty non trivial set
K10( the carrier of X) is set
the carrier of X0 is set
D is Element of K10( the carrier of X)
C is Element of K10( the carrier of X)
B is Element of K10( the carrier of X)
D /\ B is Element of K10( the carrier of X)
C \/ (D /\ B) is Element of K10( the carrier of X)
C \/ B is Element of K10( the carrier of X)
X1 is non empty strict TopSpace-like open (X) (X) (X) (X) SubSpace of X
the carrier of X1 is non empty set
X2 is non empty strict TopSpace-like closed non open proper (X) (X) (X) (X) SubSpace of X
the carrier of X2 is non empty set
X1 is strict TopSpace-like non closed open proper (X) (X) (X) (X) SubSpace of X
the carrier of X1 is set
c9 is Element of K10( the carrier of X)
c10 is Element of K10( the carrier of X)