:: TEX_3 semantic presentation

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

c

c

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

c

c