:: TEX_2 semantic presentation

K119() is set

K123() is non empty V24() V25() V26() V31() cardinal limit_cardinal Element of bool K119()

bool K119() is non empty set

K96() is non empty V24() V25() V26() V31() cardinal limit_cardinal set

bool K96() is non empty V31() set

bool K123() is non empty V31() set

2 is non empty V24() V25() V26() V30() V31() cardinal Element of K123()

[:2,2:] is non empty Relation-like set

[:[:2,2:],2:] is non empty Relation-like set

bool [:[:2,2:],2:] is non empty set

I[01] is non empty strict TopSpace-like TopStruct

the carrier of I[01] is non empty set

{} is empty trivial Relation-like non-empty empty-yielding Function-like one-to-one constant functional V24() V25() V26() V28() V29() V30() V31() cardinal {} -element set

the empty trivial Relation-like non-empty empty-yielding Function-like one-to-one constant functional V24() V25() V26() V28() V29() V30() V31() cardinal {} -element set is empty trivial Relation-like non-empty empty-yielding Function-like one-to-one constant functional V24() V25() V26() V28() V29() V30() V31() cardinal {} -element set

1 is non empty V24() V25() V26() V30() V31() cardinal Element of K123()

X is non empty set

X0 is non empty trivial 1 -element set

Z0 is Element of X0

{Z0} is non empty trivial 1 -element Element of bool X0

bool X0 is non empty set

X is non empty trivial 1 -element set

X0 is set

X /\ X0 is set

Z0 is set

{Z0} is non empty trivial 1 -element set

Z0 is Element of X

{Z0} is non empty trivial 1 -element Element of bool X

bool X is non empty set

X is non empty trivial 1 -element set

bool X is non empty set

X0 is trivial Element of bool X

Z0 is Element of X

{Z0} is non empty trivial 1 -element Element of bool X

X0 is trivial Element of bool X

X is non empty set

X0 is Element of X

{X0} is non empty trivial 1 -element Element of bool X

bool X is non empty set

X is non empty non trivial set

X0 is Element of X

{X0} is non empty trivial 1 -element Element of bool X

bool X is non empty set

X is non empty trivial 1 -element set

bool X is non empty set

X0 is non empty trivial non proper 1 -element Element of bool X

X is non empty non trivial set

bool X is non empty set

X0 is non empty Element of bool X

X0 is non empty Element of bool X

X is non empty non trivial set

bool X is non empty set

the non empty trivial proper 1 -element Element of bool X is non empty trivial proper 1 -element Element of bool X

[#] X is non empty non trivial non proper Element of bool X

X is non empty 1-sorted

the carrier of X is non empty set

X0 is Element of the carrier of X

{X0} is non empty trivial 1 -element Element of bool the carrier of X

bool the carrier of X is non empty set

X is non empty non trivial 1-sorted

the carrier of X is non empty non trivial set

X0 is Element of the carrier of X

{X0} is non empty trivial proper 1 -element Element of bool the carrier of X

bool the carrier of X is non empty set

X is non empty trivial V46() 1 -element 1-sorted

the carrier of X is non empty trivial V31() 1 -element set

bool the carrier of X is non empty set

X0 is non empty trivial non proper 1 -element Element of bool the carrier of X

X0 is non empty trivial non proper 1 -element Element of bool the carrier of X

X is non empty non trivial 1-sorted

the carrier of X is non empty non trivial set

bool the carrier of X is non empty set

X0 is non empty Element of bool the carrier of X

X0 is non empty Element of bool the carrier of X

X is non empty non trivial 1-sorted

the carrier of X is non empty non trivial set

bool the carrier of X is non empty set

the non empty trivial proper 1 -element Element of bool the carrier of X is non empty trivial proper 1 -element Element of bool the carrier of X

[#] X is non empty non trivial non proper Element of bool the carrier of X

X is non empty non trivial 1-sorted

the carrier of X is non empty non trivial set

bool the carrier of X is non empty set

the non empty trivial proper 1 -element Element of bool the carrier of X is non empty trivial proper 1 -element Element of bool the carrier of X

Z0 is Element of bool the carrier of X

X is non empty set

bool X is non empty set

X0 is proper Element of bool X

X0 ` is Element of bool X

X \ X0 is set

(X0 `) ` is Element of bool X

X \ (X0 `) is set

X is TopStruct

the carrier of X is set

the topology of X is open Element of bool (bool the carrier of X)

bool the carrier of X is non empty set

bool (bool the carrier of X) is non empty set

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

X0 is TopStruct

the carrier of X0 is set

the topology of X0 is open Element of bool (bool the carrier of X0)

bool the carrier of X0 is non empty set

bool (bool the carrier of X0) is non empty set

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

Z0 is Element of bool (bool the carrier of X0)

union Z0 is Element of bool the carrier of X0

Z0 is Element of bool the carrier of X0

Z1 is Element of bool the carrier of X0

Z0 /\ Z1 is Element of bool the carrier of X0

X is TopStruct

X is TopStruct

the carrier of X is set

bool the carrier of X is non empty set

X0 is SubSpace of X

the carrier of X0 is set

Z0 is Element of bool the carrier of X

Z0 is Element of bool the carrier of X

X is TopStruct

X0 is SubSpace of X

[#] X0 is non proper dense Element of bool the carrier of X0

the carrier of X0 is set

bool the carrier of X0 is non empty set

[#] X is non proper dense Element of bool the carrier of X

the carrier of X is set

bool the carrier of X is non empty set

X is TopStruct

X0 is SubSpace of X

the carrier of X0 is set

the topology of X0 is open Element of bool (bool the carrier of X0)

bool the carrier of X0 is non empty set

bool (bool the carrier of X0) is non empty set

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

Z0 is SubSpace of X

the carrier of Z0 is set

the topology of Z0 is open Element of bool (bool the carrier of Z0)

bool the carrier of Z0 is non empty set

bool (bool the carrier of Z0) is non empty set

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

the carrier of X is set

bool the carrier of X is non empty set

Z0 is Element of bool the carrier of X

X is TopStruct

the carrier of X is set

X0 is SubSpace of X

the carrier of X0 is set

bool the carrier of X is non empty set

Z0 is Element of bool the carrier of X

Z0 is Element of bool the carrier of X

Z0 is Element of bool the carrier of X

X is non empty trivial V46() 1 -element TopStruct

X0 is non empty SubSpace of X

the carrier of X is non empty trivial V31() 1 -element set

bool the carrier of X is non empty set

the carrier of X0 is non empty set

Z0 is non empty trivial non proper 1 -element Element of bool the carrier of X

Z0 is non empty trivial non proper 1 -element Element of bool the carrier of X

Z0 is non empty trivial non proper 1 -element Element of bool the carrier of X

X0 is non empty (X) SubSpace of X

the carrier of X is non empty trivial V31() 1 -element set

bool the carrier of X is non empty set

the carrier of X0 is non empty set

Z0 is trivial Element of bool the carrier of X

Z0 is non empty trivial non proper 1 -element Element of bool the carrier of X

X is non empty non trivial TopStruct

X0 is non empty SubSpace of X

the carrier of X is non empty non trivial set

bool the carrier of X is non empty set

the carrier of X0 is non empty set

Z0 is Element of bool the carrier of X

X0 is non empty SubSpace of X

X is non empty TopStruct

[#] X is non empty non proper dense Element of bool the carrier of X

the carrier of X is non empty set

bool the carrier of X is non empty set

X0 is non empty Element of bool the carrier of X

X | X0 is non empty strict SubSpace of X

[#] (X | X0) is non empty non proper dense Element of bool the carrier of (X | X0)

the carrier of (X | X0) is non empty set

bool the carrier of (X | X0) is non empty set

X is non empty TopStruct

the carrier of X is non empty set

the topology of X is open Element of bool (bool the carrier of X)

bool the carrier of X is non empty set

bool (bool the carrier of X) is non empty set

TopStruct(# the carrier of X, the topology of X #) is non empty strict TopStruct

X0 is (X) SubSpace of X

the carrier of X0 is set

the topology of X0 is open Element of bool (bool the carrier of X0)

bool the carrier of X0 is non empty set

bool (bool the carrier of X0) is non empty set

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

Z0 is set

Z0 is Element of bool the carrier of X

Z1 is Element of bool the carrier of X

Z1 is Element of bool the carrier of X

Z1 is Element of bool the carrier of X0

[#] X0 is non proper dense Element of bool the carrier of X0

Z1 /\ ([#] X0) is Element of bool the carrier of X0

Z1 is Element of bool the carrier of X

Z1 /\ ([#] X0) is Element of bool the carrier of X0

Z0 is Element of bool the carrier of X

Z0 is set

Z0 is Element of bool the carrier of X0

Z1 is Element of bool the carrier of X

Z1 /\ ([#] X0) is Element of bool the carrier of X0

Z0 is Element of bool the carrier of X

X is non empty TopStruct

X0 is SubSpace of X

X0 is SubSpace of X

X0 is SubSpace of X

X0 is SubSpace of X

X is TopStruct

the carrier of X is set

the topology of X is open Element of bool (bool the carrier of X)

bool the carrier of X is non empty set

bool (bool the carrier of X) is non empty set

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

X0 is TopStruct

the carrier of X0 is set

the topology of X0 is open Element of bool (bool the carrier of X0)

bool the carrier of X0 is non empty set

bool (bool the carrier of X0) is non empty set

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

bool the carrier of X is non empty Element of bool (bool the carrier of X)

X is TopStruct

the carrier of X is set

the topology of X is open Element of bool (bool the carrier of X)

bool the carrier of X is non empty set

bool (bool the carrier of X) is non empty set

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

X0 is TopStruct

the carrier of X0 is set

the topology of X0 is open Element of bool (bool the carrier of X0)

bool the carrier of X0 is non empty set

bool (bool the carrier of X0) is non empty set

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

{{}, the carrier of X} is non empty set

X is non empty TopStruct

X0 is SubSpace of X

X0 is SubSpace of X

X0 is SubSpace of X

X0 is SubSpace of X

X is TopStruct

the carrier of X is set

the topology of X is open Element of bool (bool the carrier of X)

bool the carrier of X is non empty set

bool (bool the carrier of X) is non empty set

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

X0 is TopStruct

the carrier of X0 is set

the topology of X0 is open Element of bool (bool the carrier of X0)

bool the carrier of X0 is non empty set

bool (bool the carrier of X0) is non empty set

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

Z0 is Element of bool the carrier of X

the carrier of X \ Z0 is Element of bool the carrier of X

X is non empty TopStruct

X0 is non empty SubSpace of X

X0 is non empty SubSpace of X

X0 is non empty SubSpace of X

X is non empty TopStruct

the carrier of X is non empty set

X0 is Element of the carrier of X

{X0} is non empty trivial 1 -element Element of bool the carrier of X

bool the carrier of X is non empty set

Z0 is non empty Element of bool the carrier of X

X | Z0 is non empty strict SubSpace of X

the carrier of (X | Z0) is non empty set

[#] (X | Z0) is non empty non proper dense Element of bool the carrier of (X | Z0)

bool the carrier of (X | Z0) is non empty set

Z0 is non empty strict SubSpace of X

the carrier of Z0 is non empty set

Z0 is non empty strict SubSpace of X

the carrier of Z0 is non empty set

[#] Z0 is non empty non proper dense Element of bool the carrier of Z0

bool the carrier of Z0 is non empty set

[#] Z0 is non empty non proper dense Element of bool the carrier of Z0

bool the carrier of Z0 is non empty set

[#] X is non empty non proper dense Element of bool the carrier of X

X1 is Element of bool the carrier of X

X | X1 is strict SubSpace of X

X is non empty TopStruct

the carrier of X is non empty set

X0 is Element of the carrier of X

(X,X0) is non empty strict SubSpace of X

the carrier of (X,X0) is non empty set

{X0} is non empty trivial 1 -element Element of bool the carrier of X

bool the carrier of X is non empty set

Z0 is Element of the carrier of (X,X0)

{Z0} is non empty trivial 1 -element Element of bool the carrier of (X,X0)

bool the carrier of (X,X0) is non empty set

X is non empty TopStruct

the carrier of X is non empty set

the Element of the carrier of X is Element of the carrier of X

(X, the Element of the carrier of X) is non empty strict SubSpace of X

X is non empty TopStruct

the carrier of X is non empty set

X0 is Element of the carrier of X

(X,X0) is non empty strict SubSpace of X

X is non empty TopStruct

the carrier of X is non empty set

X0 is Element of the carrier of X

(X,X0) is non empty trivial V46() 1 -element strict SubSpace of X

{X0} is non empty trivial 1 -element Element of bool the carrier of X

bool the carrier of X is non empty set

the carrier of (X,X0) is non empty trivial V31() 1 -element set

Z0 is Element of bool the carrier of X

Z0 is Element of bool the carrier of X

X is non empty TopStruct

the carrier of X is non empty set

X0 is Element of the carrier of X

(X,X0) is non empty trivial V46() 1 -element strict SubSpace of X

X is non empty non trivial TopStruct

the non empty trivial V46() 1 -element strict (X) SubSpace of X is non empty trivial V46() 1 -element strict (X) SubSpace of X

X is non empty TopStruct

the non empty trivial V46() 1 -element SubSpace of X is non empty trivial V46() 1 -element SubSpace of X

X0 is non empty trivial V46() 1 -element SubSpace of X

X is non empty TopStruct

the carrier of X is non empty set

X0 is non empty trivial V46() 1 -element SubSpace of X

the carrier of X0 is non empty trivial V31() 1 -element set

the topology of X0 is open Element of bool (bool the carrier of X0)

bool the carrier of X0 is non empty set

bool (bool the carrier of X0) is non empty set

TopStruct(# the carrier of X0, the topology of X0 #) is non empty strict TopStruct

Z0 is Element of the carrier of X0

{Z0} is non empty trivial non proper 1 -element Element of bool the carrier of X0

bool the carrier of X is non empty set

Z0 is Element of the carrier of X

(X,Z0) is non empty trivial V46() 1 -element strict SubSpace of X

the carrier of (X,Z0) is non empty trivial V31() 1 -element set

the topology of (X,Z0) is open Element of bool (bool the carrier of (X,Z0))

bool the carrier of (X,Z0) is non empty set

bool (bool the carrier of (X,Z0)) is non empty set

TopStruct(# the carrier of (X,Z0), the topology of (X,Z0) #) is non empty strict TopStruct

X is non empty TopStruct

the carrier of X is non empty set

X0 is Element of the carrier of X

(X,X0) is non empty trivial V46() 1 -element strict SubSpace of X

X is non empty TopStruct

X0 is non empty SubSpace of X

X is non empty TopSpace-like TopStruct

the carrier of X is non empty set

the Element of the carrier of X is Element of the carrier of X

(X, the Element of the carrier of X) is non empty trivial V46() 1 -element strict TopSpace-like compact discrete anti-discrete almost_discrete extremally_disconnected hereditarily_extremally_disconnected SubSpace of X

X is non empty TopSpace-like TopStruct

the carrier of X is non empty set

X0 is Element of the carrier of X

(X,X0) is non empty trivial V46() 1 -element strict TopSpace-like compact discrete anti-discrete almost_discrete extremally_disconnected hereditarily_extremally_disconnected SubSpace of X

X is non empty TopSpace-like TopStruct

the carrier of X is non empty set

the Element of the carrier of X is Element of the carrier of X

(X, the Element of the carrier of X) is non empty trivial V46() 1 -element strict TopSpace-like compact discrete anti-discrete almost_discrete extremally_disconnected hereditarily_extremally_disconnected SubSpace of X

X is non empty TopSpace-like TopStruct

the carrier of X is non empty set

X0 is Element of the carrier of X

(X,X0) is non empty trivial V46() 1 -element strict TopSpace-like compact discrete anti-discrete almost_discrete extremally_disconnected hereditarily_extremally_disconnected SubSpace of X

X is non empty TopSpace-like TopStruct

X0 is TopSpace-like SubSpace of X

the carrier of X is non empty set

bool the carrier of X is non empty set

the carrier of X0 is set

Z0 is Element of bool the carrier of X

[#] X is non empty non proper open closed dense non boundary Element of bool the carrier of X

Z0 is Element of bool the carrier of X

Z0 is Element of bool the carrier of X

Z0 is Element of bool 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 strict TopSpace-like closed open (X) SubSpace of X is strict TopSpace-like closed open (X) 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 SubSpace of X

X0 is non empty TopSpace-like closed open discrete almost_discrete extremally_disconnected hereditarily_extremally_disconnected 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 (X) SubSpace of X is strict TopSpace-like closed open discrete almost_discrete (X) SubSpace of X

X is non empty TopSpace-like anti-discrete almost_discrete extremally_disconnected hereditarily_extremally_disconnected TopStruct

X0 is non empty TopSpace-like anti-discrete almost_discrete extremally_disconnected hereditarily_extremally_disconnected SubSpace of X

X0 is non empty TopSpace-like anti-discrete almost_discrete extremally_disconnected hereditarily_extremally_disconnected SubSpace of X

X is non empty non trivial TopSpace-like anti-discrete almost_discrete extremally_disconnected hereditarily_extremally_disconnected TopStruct

X0 is non empty TopSpace-like anti-discrete almost_discrete extremally_disconnected hereditarily_extremally_disconnected (X) SubSpace of X

the carrier of X is non empty non trivial set

bool the carrier of X is non empty set

the carrier of X0 is non empty set

Z0 is non empty Element of bool the carrier of X

Z0 ` is Element of bool the carrier of X

the carrier of X \ Z0 is set

the topology of X is non empty open Element of bool (bool the carrier of X)

bool (bool the carrier of X) is non empty set

{{}, the carrier of X} is non empty set

the topology of X is non empty open Element of bool (bool the carrier of X)

bool (bool the carrier of X) is non empty set

{{}, the carrier of X} is non empty set

X0 is non empty trivial V46() 1 -element TopSpace-like compact non closed non open discrete anti-discrete almost_discrete extremally_disconnected hereditarily_extremally_disconnected (X) SubSpace of X

Z0 is non empty trivial V46() 1 -element TopSpace-like compact non closed non open discrete anti-discrete almost_discrete extremally_disconnected hereditarily_extremally_disconnected (X) SubSpace of X

X is non empty non trivial TopSpace-like anti-discrete almost_discrete extremally_disconnected hereditarily_extremally_disconnected TopStruct

the non empty strict TopSpace-like non closed non open anti-discrete almost_discrete extremally_disconnected hereditarily_extremally_disconnected (X) SubSpace of X is non empty strict TopSpace-like non closed non open anti-discrete 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 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 TopStruct

the carrier of X is set

bool the carrier of X is non empty set

X is TopStruct

the carrier of X is set

bool the carrier of X is non empty set

X0 is Element of bool the carrier of X

Z0 is Element of bool the carrier of X

X0 \ Z0 is Element of bool the carrier of X

Z0 is Element of bool the carrier of X

X0 /\ Z0 is Element of bool the carrier of X

[#] X is non proper dense Element of bool the carrier of X

([#] X) \ Z0 is Element of bool the carrier of X

Z1 is Element of bool the carrier of X

([#] X) \ Z1 is Element of bool the carrier of X

X0 /\ ([#] X) is Element of bool the carrier of X

X0 /\ Z1 is Element of bool the carrier of X

X0 \ Z0 is Element of bool the carrier of X

X0 \ (X0 \ Z0) is Element of bool the carrier of X

X0 /\ Z0 is Element of bool the carrier of X

Z1 is Element of bool the carrier of X

X0 /\ Z1 is Element of bool the carrier of X

Z0 is Element of bool the carrier of X

X0 \ Z0 is Element of bool the carrier of X

Z0 is Element of bool the carrier of X

X0 /\ Z0 is Element of bool the carrier of X

([#] X) \ Z0 is Element of bool the carrier of X

Z1 is Element of bool the carrier of X

X0 /\ Z1 is Element of bool the carrier of X

X0 \ Z0 is Element of bool the carrier of X

X0 \ (X0 \ Z0) is Element of bool the carrier of X

X0 /\ Z0 is Element of bool the carrier of X

Z1 is Element of bool the carrier of X

X0 /\ Z1 is Element of bool the carrier of X

X is TopStruct

the carrier of X is set

bool the carrier of X is non empty set

X0 is TopStruct

the carrier of X0 is set

bool the carrier of X0 is non empty set

the topology of X is open Element of bool (bool the carrier of X)

bool (bool the carrier of X) is non empty set

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

the topology of X0 is open Element of bool (bool the carrier of X0)

bool (bool the carrier of X0) is non empty set

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

Z0 is Element of bool the carrier of X

Z0 is Element of bool the carrier of X0

Z1 is Element of bool the carrier of X0

Z1 is Element of bool the carrier of X

X1 is Element of bool the carrier of X

Z0 /\ X1 is Element of bool the carrier of X

g is Element of bool the carrier of X0

g is Element of bool the carrier of X0

Z0 /\ g is Element of bool the carrier of X0

g is Element of bool the carrier of X0

Z0 /\ g is Element of bool the carrier of X0

X is non empty TopStruct

the carrier of X is non empty set

bool the carrier of X is non empty set

X0 is non empty SubSpace of X

the carrier of X0 is non empty set

Z0 is Element of bool the carrier of X

[#] X is non empty non proper dense Element of bool the carrier of X

[#] X0 is non empty non proper dense Element of bool the carrier of X0

bool the carrier of X0 is non empty set

Z0 is set

bool the carrier of X0 is non empty Element of bool (bool the carrier of X0)

bool (bool the carrier of X0) is non empty set

Z1 is Element of bool the carrier of X0

Z1 is Element of bool the carrier of X

X1 is Element of bool the carrier of X

Z0 /\ X1 is Element of bool the carrier of X

g is Element of bool the carrier of X

the topology of X is open Element of bool (bool the carrier of X)

bool (bool the carrier of X) is non empty set

g /\ ([#] X0) is Element of bool the carrier of X0

the topology of X0 is open Element of bool (bool the carrier of X0)

g is Element of bool the carrier of X

g /\ ([#] X0) is Element of bool the carrier of X0

Z0 is Element of bool the carrier of X

Z1 is Element of bool the carrier of X0

Z1 is Element of bool the carrier of X

Z1 /\ ([#] X0) is Element of bool the carrier of X0

X1 is Element of bool the carrier of X

g is Element of bool the carrier of X

Z0 /\ g is Element of bool the carrier of X

X is non empty TopStruct

the carrier of X is non empty set

bool the carrier of X is non empty set

X0 is Element of bool the carrier of X

Z0 is set

bool the carrier of X is non empty Element of bool (bool the carrier of X)

bool (bool the carrier of X) is non empty set

Z0 is Element of bool the carrier of X

Z1 is Element of bool the carrier of X

X0 /\ Z1 is Element of bool the carrier of X

the topology of X is open Element of bool (bool the carrier of X)

Z0 is non empty TopSpace-like discrete almost_discrete extremally_disconnected hereditarily_extremally_disconnected TopStruct

the carrier of Z0 is non empty set

bool the carrier of Z0 is non empty set

Z0 is Element of bool the carrier of Z0

Z1 is Element of bool the carrier of Z0

Z1 is Element of bool the carrier of Z0

X0 /\ Z1 is Element of bool the carrier of Z0

X is TopStruct

the carrier of X is set

bool the carrier of X is non empty set

Z0 is Element of bool the carrier of X

X0 is Element of bool the carrier of X

Z0 is Element of bool the carrier of X

Z1 is Element of bool the carrier of X

X0 /\ Z1 is Element of bool the carrier of X

Z1 is Element of bool the carrier of X

Z0 /\ Z1 is Element of bool the carrier of X

X0 /\ Z1 is Element of bool the carrier of X

X is TopStruct

the carrier of X is set

bool the carrier of X is non empty set

X0 is Element of bool the carrier of X

Z0 is Element of bool the carrier of X

X0 /\ Z0 is Element of bool the carrier of X

X is TopStruct

the carrier of X is set

bool the carrier of X is non empty set

X0 is Element of bool the carrier of X

Z0 is Element of bool the carrier of X

X0 \/ Z0 is Element of bool the carrier of X

Z0 is Element of bool the carrier of X

Z0 /\ X0 is Element of bool the carrier of X

Z1 is Element of bool the carrier of X

X0 /\ Z1 is Element of bool the carrier of X

Z0 /\ Z0 is Element of bool the carrier of X

Z1 is Element of bool the carrier of X

Z0 /\ Z1 is Element of bool the carrier of X

Z0 /\ (X0 \/ Z0) is Element of bool the carrier of X

(X0 /\ Z1) \/ (Z0 /\ Z1) is Element of bool the carrier of X

X1 is Element of bool the carrier of X

(X0 \/ Z0) /\ X1 is Element of bool the carrier of X

X1 is Element of bool the carrier of X

(X0 \/ Z0) /\ X1 is Element of bool the carrier of X

X is TopStruct

the carrier of X is set

bool the carrier of X is non empty set

X0 is Element of bool the carrier of X

Z0 is Element of bool the carrier of X

X0 \/ Z0 is Element of bool the carrier of X

Z0 is Element of bool the carrier of X

Z0 /\ X0 is Element of bool the carrier of X

Z1 is Element of bool the carrier of X

X0 /\ Z1 is Element of bool the carrier of X

Z0 /\ Z0 is Element of bool the carrier of X

Z1 is Element of bool the carrier of X

Z0 /\ Z1 is Element of bool the carrier of X

Z0 /\ (X0 \/ Z0) is Element of bool the carrier of X

(X0 /\ Z1) \/ (Z0 /\ Z1) is Element of bool the carrier of X

X1 is Element of bool the carrier of X

(X0 \/ Z0) /\ X1 is Element of bool the carrier of X

X1 is Element of bool the carrier of X

(X0 \/ Z0) /\ X1 is Element of bool the carrier of X

X is TopStruct

the carrier of X is set

bool the carrier of X is non empty set

X0 is Element of bool the carrier of X

Z0 is Element of the carrier of X

{Z0} is non empty trivial 1 -element set

Z0 is non empty TopStruct

the carrier of Z0 is non empty set

bool the carrier of Z0 is non empty set

Z1 is Element of bool the carrier of Z0

Z1 is Element of bool the carrier of Z0

X1 is Element of bool the carrier of Z0

Z1 /\ X1 is Element of bool the carrier of Z0

g is Element of bool the carrier of X

X0 /\ g is Element of bool the carrier of X

X is TopStruct

the carrier of X is set

bool the carrier of X is non empty set

X0 is Element of bool the carrier of X

Z0 is Element of the carrier of X

{Z0} is non empty trivial 1 -element set

Z0 is non empty TopStruct

the carrier of Z0 is non empty set

bool the carrier of Z0 is non empty set

Z1 is Element of bool the carrier of Z0

Z1 is Element of bool the carrier of Z0

X1 is Element of bool the carrier of X

Z1 /\ X1 is Element of bool the carrier of X

X0 /\ X1 is Element of bool the carrier of X

X is non empty TopSpace-like TopStruct

the carrier of X is non empty set

bool the carrier of X is non empty set

X0 is non empty Element of bool the carrier of X

Z0 is non empty strict TopSpace-like SubSpace of X

the carrier of Z0 is non empty set

Z0 is non empty strict TopSpace-like discrete almost_discrete extremally_disconnected hereditarily_extremally_disconnected SubSpace of X

the carrier of Z0 is non empty set

X is non empty TopSpace-like TopStruct

the carrier of X is non empty set

bool the carrier of X is non empty set

X0 is empty trivial proper Relation-like non-empty empty-yielding Function-like one-to-one constant functional V24() V25() V26() V28() V29() V30() V31() cardinal {} -element open closed boundary nowhere_dense compact Element of bool the carrier of X

Z0 is Element of bool the carrier of X

{} X is empty trivial proper Relation-like non-empty empty-yielding Function-like one-to-one constant functional V24() V25() V26() V28() V29() V30() V31() cardinal {} -element open closed boundary nowhere_dense compact Element of bool the carrier of X

Z0 is empty trivial proper Relation-like non-empty empty-yielding Function-like one-to-one constant functional V24() V25() V26() V28() V29() V30() V31() cardinal {} -element open closed boundary nowhere_dense compact Element of bool the carrier of X

X0 /\ Z0 is Relation-like open closed Element of bool the carrier of X

Z0 is empty trivial proper Relation-like non-empty empty-yielding Function-like one-to-one constant functional V24() V25() V26() V28() V29() V30() V31() cardinal {} -element open closed boundary nowhere_dense compact Element of bool the carrier of X

X0 /\ Z0 is Relation-like open closed Element of bool the carrier of X

X is non empty TopSpace-like TopStruct

the carrier of X is non empty set

X0 is Element of the carrier of X

{X0} is non empty trivial 1 -element compact Element of bool the carrier of X

bool the carrier of X is non empty set

Z0 is Element of bool the carrier of X

{} X is empty trivial proper Relation-like non-empty empty-yielding Function-like one-to-one constant functional V24() V25() V26() V28() V29() V30() V31() cardinal {} -element open closed boundary nowhere_dense compact Element of bool the carrier of X

Z0 is empty trivial proper Relation-like non-empty empty-yielding Function-like one-to-one constant functional V24() V25() V26() V28() V29() V30() V31() cardinal {} -element open closed boundary nowhere_dense compact Element of bool the carrier of X

{X0} /\ Z0 is Relation-like Element of bool the carrier of X

[#] X is non empty non proper open closed dense non boundary Element of bool the carrier of X

Z0 is non empty non proper open closed dense non boundary Element of bool the carrier of X

{X0} /\ Z0 is Element of bool the carrier of X

Z0 is empty trivial proper Relation-like non-empty empty-yielding Function-like one-to-one constant functional V24() V25() V26() V28() V29() V30() V31() cardinal {} -element open closed boundary nowhere_dense compact Element of bool the carrier of X

{X0} /\ Z0 is Relation-like Element of bool the carrier of X

Z1 is non empty non proper open closed dense non boundary Element of bool the carrier of X

{X0} /\ Z1 is Element of bool the carrier of X

X is non empty TopSpace-like TopStruct

the carrier of X is non empty set

bool the carrier of X is non empty set

X0 is Element of bool the carrier of X

Z0 is non empty strict TopSpace-like SubSpace of X

the carrier of Z0 is non empty set

[#] X is non empty non proper open closed dense non boundary Element of bool the carrier of X

[#] Z0 is non empty non proper open closed dense non boundary Element of bool the carrier of Z0

bool the carrier of Z0 is non empty set

Z1 is Element of the carrier of Z0

Z1 is Element of the carrier of X

{Z1} is non empty trivial 1 -element compact Element of bool the carrier of X

X1 is Element of bool the carrier of X

X0 /\ X1 is Element of bool the carrier of X

Z0 is Element of bool the carrier of Z0

{Z1} is non empty trivial 1 -element compact Element of bool the carrier of Z0

g is Element of bool the carrier of X

the topology of X is non empty open Element of bool (bool the carrier of X)

bool (bool the carrier of X) is non empty set

g /\ ([#] Z0) is Element of bool the carrier of Z0

the topology of Z0 is non empty open Element of bool (bool the carrier of Z0)

bool (bool the carrier of Z0) is non empty set

g is Element of bool the carrier of X

g /\ ([#] Z0) is Element of bool the carrier of Z0

X is non empty TopSpace-like TopStruct

the carrier of X is non empty set

bool the carrier of X is non empty set

X0 is Element of bool the carrier of X

Z0 is Element of bool the carrier of X

X0 \/ Z0 is Element of bool the carrier of X

Z0 is Element of bool the carrier of X

Z1 is Element of bool the carrier of X

Z0 /\ Z1 is Element of bool the carrier of X

Z0 \/ Z1 is Element of bool the carrier of X

X is non empty TopSpace-like TopStruct

the carrier of X is non empty set

bool the carrier of X is non empty set

X0 is Element of bool the carrier of X

Z0 is Element of bool the carrier of X

X0 \/ Z0 is Element of bool the carrier of X

Z0 is Element of bool the carrier of X

Z1 is Element of bool the carrier of X

Z0 /\ Z1 is Element of bool the carrier of X

Z0 \/ Z1 is Element of bool the carrier of X

X is set

X0 is set

X0 \ X is Element of bool X0

bool X0 is non empty set

X \/ (X0 \ X) is set

X is non empty TopSpace-like TopStruct

the carrier of X is non empty set

bool the carrier of X is non empty set

X0 is Element of bool the carrier of X

Int X0 is open Element of bool the carrier of X

Cl (Int X0) is closed Element of bool the carrier of X

X0 \ (Int X0) is Element of bool the carrier of X

Z0 is set

Z0 is Element of the carrier of X

{Z0} is non empty trivial 1 -element compact Element of bool the carrier of X

Z1 is Element of bool the carrier of X

X0 /\ Z1 is Element of bool the carrier of X

(Int X0) /\ Z1 is Element of bool the carrier of X

(Cl (Int X0)) /\ Z1 is Element of bool the carrier of X

X is non empty TopSpace-like TopStruct

the carrier of X is non empty set

bool the carrier of X is non empty set

X0 is Element of bool the carrier of X

Z0 is Element of bool the carrier of X

Cl Z0 is closed Element of bool the carrier of X

X0 /\ (Cl Z0) is Element of bool the carrier of X

Z0 is Element of bool the carrier of X

X0 /\ Z0 is Element of bool the carrier of X

Z0 is Element of bool the carrier of X

Cl Z0 is closed Element of bool the carrier of X

Z0 is closed Element of bool the carrier of X

X0 /\ Z0 is Element of bool the carrier of X

Z0 is closed Element of bool the carrier of X

X0 /\ Z0 is Element of bool the carrier of X

X is non empty TopSpace-like TopStruct

the carrier of X is non empty set

bool the carrier of X is non empty set

X0 is Element of bool the carrier of X

Z0 is Element of the carrier of X

{Z0} is non empty trivial 1 -element compact Element of bool the carrier of X

Cl {Z0} is closed Element of bool the carrier of X

X0 /\ (Cl {Z0}) is Element of bool the carrier of X

X is non empty TopSpace-like discrete almost_discrete extremally_disconnected hereditarily_extremally_disconnected TopStruct

the carrier of X is non empty set

bool the carrier of X is non empty set

X0 is Element of bool the carrier of X

Z0 is non empty strict TopSpace-like closed open discrete almost_discrete extremally_disconnected hereditarily_extremally_disconnected SubSpace of X

the carrier of Z0 is non empty set

X is non empty TopSpace-like anti-discrete almost_discrete extremally_disconnected hereditarily_extremally_disconnected TopStruct

the carrier of X is non empty set

bool the carrier of X is non empty set

X0 is non empty Element of bool the carrier of X

Z0 is set

Z0 is Element of the carrier of X

{Z0} is non empty trivial 1 -element compact Element of bool the carrier of X

Z1 is Element of bool the carrier of X

X0 /\ Z1 is Element of bool the carrier of X

Z1 is Element of the carrier of X

{Z1} is non empty trivial 1 -element compact Element of bool the carrier of X

Z1 is Element of the carrier of X

{Z1} is non empty trivial 1 -element compact Element of bool the carrier of X

Z0 is Element of X0

{Z0} is non empty trivial 1 -element Element of bool X0

bool X0 is non empty set

X is TopStruct

the carrier of X is set

bool the carrier of X is non empty set

X is TopStruct

the carrier of X is set

bool the carrier of X is non empty set

X0 is TopStruct

the carrier of X0 is set

bool the carrier of X0 is non empty set

the topology of X is open Element of bool (bool the carrier of X)

bool (bool the carrier of X) is non empty set

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

the topology of X0 is open Element of bool (bool the carrier of X0)

bool (bool the carrier of X0) is non empty set

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

Z0 is Element of bool the carrier of X

Z0 is Element of bool the carrier of X0

Z1 is Element of bool the carrier of X0

Z1 is Element of bool the carrier of X

X is non empty TopSpace-like TopStruct

the carrier of X is non empty set

bool the carrier of X is non empty set

X0 is set

Z0 is empty trivial proper Relation-like non-empty empty-yielding Function-like one-to-one constant functional V24() V25() V26() V28() V29() V30() V31() cardinal {} -element open closed boundary nowhere_dense compact Element of bool the carrier of X

Z0 is Element of the carrier of X

{Z0} is non empty trivial 1 -element compact Element of bool the carrier of X

Z1 is non empty trivial 1 -element compact Element of bool the carrier of X

Z1 is non empty trivial 1 -element compact Element of bool the carrier of X

X is non empty TopSpace-like TopStruct

the carrier of X is non empty set

bool the carrier of X is non empty set

X0 is Element of bool the carrier of X

Cl X0 is closed Element of bool the carrier of X

the carrier of X \ (Cl X0) is Element of bool the carrier of X

Z0 is set

Z0 is Element of the carrier of X

{Z0} is non empty trivial 1 -element compact Element of bool the carrier of X

X0 \/ {Z0} is non empty Element of bool the carrier of X

Z1 is Element of the carrier of X

{Z1} is non empty trivial 1 -element compact Element of bool the carrier of X

X1 is non empty trivial 1 -element compact Element of bool the carrier of X

g is Element of bool the carrier of X

X0 /\ g is Element of bool the carrier of X

(X0 \/ {Z0}) /\ X1 is Element of bool the carrier of X

X1 is non empty trivial 1 -element compact Element of bool the carrier of X

(X0 \/ {Z0}) /\ X1 is Element of bool the carrier of X

[#] X is non empty non proper open closed dense non boundary Element of bool the carrier of X

([#] X) \ (Cl X0) is Element of bool the carrier of X

X1 is Element of bool the carrier of X

(X0 \/ {Z0}) /\ X1 is Element of bool the carrier of X

X0 /\ X1 is Element of bool the carrier of X

{Z0} /\ X1 is Element of bool the carrier of X

(X0 /\ X1) \/ ({Z0} /\ X1) is Element of bool the carrier of X

(Cl X0) ` is open Element of bool the carrier of X

the carrier of X \ (Cl X0) is set

{Z1} is non empty trivial 1 -element compact Element of bool the carrier of X

X1 is Element of bool the carrier of X

(X0 \/ {Z0}) /\ X1 is Element of bool the carrier of X

{Z1} is non empty trivial 1 -element compact Element of bool the carrier of X

{Z1} is non empty trivial 1 -element compact Element of bool the carrier of X

X1 is Element of bool the carrier of X

(X0 \/ {Z0}) /\ X1 is Element of bool the carrier of X

Z1 is Element of bool the carrier of X

X is non empty TopSpace-like TopStruct

the carrier of X is non empty set

bool the carrier of X is non empty set

X0 is Element of bool the carrier of X

Z0 is Element of bool the carrier of X

Z0 \ X0 is Element of bool the carrier of X

Z0 is set

Z1 is Element of the carrier of X

{Z1} is non empty trivial 1 -element compact Element of bool the carrier of X

Z1 is Element of bool the carrier of X

Z0 /\ Z1 is Element of bool the carrier of X

X0 /\ Z1 is Element of bool the carrier of X

Cl X0 is closed Element of bool the carrier of X

(Cl X0) /\ Z1 is Element of bool the carrier of X

X is non empty TopSpace-like discrete almost_discrete extremally_disconnected hereditarily_extremally_disconnected TopStruct

the carrier of X is non empty set

bool the carrier of X is non empty set

X0 is Element of bool the carrier of X

Z0 is Element of bool the carrier of X

Z0 is Element of bool the carrier of X

X is non empty TopSpace-like anti-discrete almost_discrete extremally_disconnected hereditarily_extremally_disconnected TopStruct

the carrier of X is non empty set

bool the carrier of X is non empty set

X0 is non empty Element of bool the carrier of X

Z0 is Element of bool the carrier of X

Z0 is non empty Element of bool the carrier of X

X is non empty TopStruct

X is non empty TopStruct

the carrier of X is non empty set

bool the carrier of X is non empty set

X0 is SubSpace of X

the carrier of X0 is set

Z0 is Element of bool the carrier of X

Z0 is Element of bool the carrier of X

X is non empty TopStruct

X0 is non empty SubSpace of X

the carrier of X is non empty set

bool the carrier of X is non empty set

the carrier of X0 is non empty set

Z0 is Element of bool the carrier of X

X0 is non empty SubSpace of X

X is non empty TopSpace-like TopStruct

X0 is non empty TopSpace-like SubSpace of X

the carrier of X0 is non empty set

the topology of X0 is non empty open Element of bool (bool the carrier of X0)

bool the carrier of X0 is non empty set

bool (bool the carrier of X0) is non empty 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

bool the carrier of X is non empty set

Z0 is Element of bool the carrier of X

Z0 is non empty TopSpace-like discrete almost_discrete extremally_disconnected hereditarily_extremally_disconnected SubSpace of X

the carrier of Z0 is non empty set

the topology of Z0 is non empty open Element of bool (bool the carrier of Z0)

bool the carrier of Z0 is non empty set

bool (bool the carrier of Z0) is non empty set

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

Z1 is Element of bool the carrier of X

Z0 is Element of bool the carrier of X

Z1 is non empty strict TopSpace-like discrete almost_discrete extremally_disconnected hereditarily_extremally_disconnected SubSpace of X

the carrier of Z1 is non empty set

X is non empty TopSpace-like TopStruct

the carrier of X is non empty set

bool the carrier of X is non empty set

X0 is non empty Element of bool the carrier of X

Z0 is non empty strict TopSpace-like SubSpace of X

the carrier of Z0 is non empty set

X is non empty TopSpace-like discrete almost_discrete extremally_disconnected hereditarily_extremally_disconnected TopStruct

X0 is TopSpace-like closed open discrete almost_discrete SubSpace of X

the carrier of X is non empty set

bool the carrier of X is non empty set

the carrier of X0 is set

Z0 is Element of bool the carrier of X

Z0 is Element of bool the carrier of X

Z0 is Element of bool the carrier 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

the carrier of X is non empty set

bool the carrier of X is non empty set

the carrier of X0 is set

Z0 is Element of bool the carrier of X

Z0 is Element of bool the carrier of X

X0 is TopSpace-like closed open discrete almost_discrete SubSpace of X

X is non empty TopSpace-like anti-discrete almost_discrete extremally_disconnected hereditarily_extremally_disconnected TopStruct

X0 is non empty TopSpace-like anti-discrete almost_discrete extremally_disconnected hereditarily_extremally_disconnected SubSpace of X

X0 is non empty TopSpace-like anti-discrete almost_discrete extremally_disconnected hereditarily_extremally_disconnected SubSpace of X

X0 is non empty TopSpace-like anti-discrete almost_discrete extremally_disconnected hereditarily_extremally_disconnected SubSpace of X

the carrier of X is non empty set

bool the carrier of X is non empty set

the carrier of X0 is non empty set

Z0 is Element of bool the carrier of X

X0 is non empty TopSpace-like anti-discrete almost_discrete extremally_disconnected hereditarily_extremally_disconnected SubSpace of X

F

the carrier of F

bool the carrier of F

bool (bool the carrier of F

F

[:F

bool [:F

X is set

X0 is Element of bool the carrier of F

Z0 is Element of the carrier of F

X is Relation-like Function-like set

dom X is set

rng X is set

X0 is Relation-like Function-like V17(F

Z0 is Element of bool the carrier of F

X0 . Z0 is set

X is non empty TopSpace-like almost_discrete extremally_disconnected hereditarily_extremally_disconnected TopStruct

the carrier of X is non empty set

bool the carrier of X is non empty set

X0 is Element of bool the carrier of X

Cl X0 is closed Element of bool the carrier of X

{ (Cl {b

union { (Cl {b

Z0 is set

bool the carrier of X is non empty Element of bool (bool the carrier of X)

bool (bool the carrier of X) is non empty set

Z1 is Element of the carrier of X

{Z1} is non empty trivial 1 -element compact Element of bool the carrier of X

Cl {Z1} is closed Element of bool the carrier of X

Z0 is Element of bool (bool the carrier of X)

Z1 is set

X1 is Element of the carrier of X

{X1} is non empty trivial 1 -element compact Element of bool the carrier of X

Cl {X1} is closed Element of bool the carrier of X

Z1 is Element of bool (bool the carrier of X)

union Z1 is Element of bool the carrier of X

Z1 is set

X1 is Element of the carrier of X

{X1} is non empty trivial 1 -element compact Element of bool the carrier of X

Cl {X1} is closed Element of bool the carrier of X

Z1 is Element of bool the carrier of X

X1 is Element of the carrier of X

{X1} is non empty trivial 1 -element compact Element of bool the carrier of X

Cl {X1} is closed Element of bool the carrier of X

X is non empty TopSpace-like almost_discrete extremally_disconnected hereditarily_extremally_disconnected TopStruct

the carrier of X is non empty set

X0 is Element of the carrier of X

Z0 is Element of the carrier of X

{Z0} is non empty trivial 1 -element compact Element of bool the carrier of X

bool the carrier of X is non empty set

Cl {Z0} is closed Element of bool the carrier of X

{X0} is non empty trivial 1 -element compact Element of bool the carrier of X

Cl {X0} is closed Element of bool the carrier of X

(Cl {Z0}) /\ (Cl {X0}) is closed Element of bool the carrier of X

X is non empty TopSpace-like almost_discrete extremally_disconnected hereditarily_extremally_disconnected TopStruct

the carrier of X is non empty set

X0 is Element of the carrier of X

{X0} is non empty trivial 1 -element compact Element of bool the carrier of X

bool the carrier of X is non empty set

Cl {X0} is closed Element of bool the carrier of X

Z0 is Element of the carrier of X

{Z0} is non empty trivial 1 -element compact Element of bool the carrier of X

Cl {Z0} is closed Element of bool the carrier of X

(Cl {X0}) /\ (Cl {Z0}) is closed Element of bool the carrier of X

Z0 is set

Z1 is Element of the carrier of X

{Z1} is non empty trivial 1 -element compact Element of bool the carrier of X

Cl {Z1} is closed Element of bool the carrier of X

X is non empty TopSpace-like almost_discrete extremally_disconnected hereditarily_extremally_disconnected TopStruct

the carrier of X is non empty set

bool the carrier of X is non empty set

X0 is Element of bool the carrier of X

Z0 is Element of the carrier of X

{Z0} is non empty trivial 1 -element compact Element of bool the carrier of X

Z0 is Element of bool the carrier of X

X0 /\ Z0 is Element of bool the carrier of X

Z1 is Element of bool the carrier of X

X0 /\ Z1 is Element of bool the carrier of X

Z0 is Element of bool the carrier of X

X0 /\ Z0 is Element of bool the carrier of X

X is non empty TopSpace-like almost_discrete extremally_disconnected hereditarily_extremally_disconnected TopStruct

the carrier of X is non empty set

bool the carrier of X is non empty set

X0 is Element of bool the carrier of X

Z0 is Element of the carrier of X

{Z0} is non empty trivial 1 -element compact Element of bool the carrier of X

Cl {Z0} is closed Element of bool the carrier of X

Z0 is closed Element of bool the carrier of X

X0 /\ Z0 is Element of bool the carrier of X

Z0 is closed Element of bool the carrier of X

X0 /\ Z0 is Element of bool the carrier of X

X is non empty TopSpace-like almost_discrete extremally_disconnected hereditarily_extremally_disconnected TopStruct

the carrier of X is non empty set

bool the carrier of X is non empty set

X0 is Element of bool the carrier of X

Z0 is Element of the carrier of X

Z0 is Element of the carrier of X

{Z0} is non empty trivial 1 -element compact Element of bool the carrier of X

Cl {Z0} is closed Element of bool the carrier of X

{Z0} is non empty trivial 1 -element compact Element of bool the carrier of X

Cl {Z0} is closed Element of bool the carrier of X

X0 /\ (Cl {Z0}) is Element of bool the carrier of X

(Cl {Z0}) /\ (Cl {Z0}) is closed Element of bool the carrier of X

X0 /\ (Cl {Z0}) is Element of bool the carrier of X

Z0 is Element of the carrier of X

{Z0} is non empty trivial 1 -element compact Element of bool the carrier of X

Cl {Z0} is closed Element of bool the carrier of X

X0 /\ (Cl {Z0}) is Element of bool the carrier of X

(X0 /\ (Cl {Z0})) \ {Z0} is Element of bool the carrier of X

Z0 is set

Z1 is Element of the carrier of X

{Z1} is non empty trivial 1 -element compact Element of bool the carrier of X

Cl {Z1} is closed Element of bool the carrier of X

(Cl {Z1}) /\ (Cl {Z0}) is closed Element of bool the carrier of X

X is non empty TopSpace-like almost_discrete extremally_disconnected hereditarily_extremally_disconnected TopStruct

the carrier of X is non empty set

bool the carrier of X is non empty set

X0 is Element of bool the carrier of X

Cl X0 is closed Element of bool the carrier of X

Z0 is Element of the carrier of X

{Z0} is non empty trivial 1 -element compact Element of bool the carrier of X

Cl {Z0} is closed Element of bool the carrier of X

X0 /\ (Cl {Z0}) is Element of bool the carrier of X

{ (Cl {b

union { (Cl {b

Z0 is set

Z1 is Element of the carrier of X

{Z1} is non empty trivial 1 -element compact Element of bool the carrier of X

Cl {Z1} is closed Element of bool the carrier of X

Z1 is Element of the carrier of X

{Z1} is non empty trivial 1 -element compact Element of bool the carrier of X

Cl {Z1} is closed Element of bool the carrier of X

Z1 is Element of the carrier of X

{Z1} is non empty trivial 1 -element compact Element of bool the carrier of X

Z0 is Element of the carrier of X

{Z0} is non empty trivial 1 -element compact Element of bool the carrier of X

Cl {Z0} is closed Element of bool the carrier of X

X0 /\ (Cl {Z0}) is Element of bool the carrier of X

Z0 is Element of the carrier of X

{Z0} is non empty trivial 1 -element compact Element of bool the carrier of X

X is non empty TopSpace-like almost_discrete extremally_disconnected hereditarily_extremally_disconnected TopStruct

the carrier of X is non empty set

bool the carrier of X is non empty set

X0 is Element of bool the carrier of X

Cl X0 is closed Element of bool the carrier of X

X is non empty TopSpace-like almost_discrete extremally_disconnected hereditarily_extremally_disconnected TopStruct

the carrier of X is non empty set

bool the carrier of X is non empty set

X0 is Element of bool the carrier of X

Cl X0 is closed Element of bool the carrier of X

the carrier of X \ (Cl X0) is Element of bool the carrier of X

Z0 is set

Z0 is Element of the carrier of X

{Z0} is non empty trivial 1 -element compact Element of bool the carrier of X

X0 \/ {Z0} is non empty Element of bool the carrier of X

Z1 is Element of the carrier of X

{Z1} is non empty trivial 1 -element compact Element of bool the carrier of X

X1 is Element of bool the carrier of X

X0 /\ X1 is Element of bool the carrier of X

(Cl X0) /\ X1 is Element of bool the carrier of X

g is Element of bool the carrier of X

(X0 \/ {Z0}) /\ g is Element of bool the carrier of X

X0 /\ g is Element of bool the carrier of X

{Z0} /\ g is Element of bool the carrier of X

(X0 /\ g) \/ ({Z0} /\ g) is Element of bool the carrier of X

g is Element of bool the carrier of X

(X0 \/ {Z0}) /\ g is Element of bool the carrier of X

[#] X is non empty non proper open closed dense non boundary Element of bool the carrier of X

([#] X) \ (Cl X0) is Element of bool the carrier of X

X1 is Element of bool the carrier of X

(X0 \/ {Z0}) /\ X1 is Element of bool the carrier of X

X0 /\ X1 is Element of bool the carrier of X

{Z0} /\ X1 is Element of bool the carrier of X

(X0 /\ X1) \/ ({Z0} /\ X1) is Element of bool the carrier of X

(Cl X0) ` is open Element of bool the carrier of X

the carrier of X \ (Cl X0) is set

{Z1} is non empty trivial 1 -element compact Element of bool the carrier of X

X1 is Element of bool the carrier of X

(X0 \/ {Z0}) /\ X1 is Element of bool the carrier of X

{Z1} is non empty trivial 1 -element compact Element of bool the carrier of X

{Z1} is non empty trivial 1 -element compact Element of bool the carrier of X

X1 is Element of bool the carrier of X

(X0 \/ {Z0}) /\ X1 is Element of bool the carrier of X

Z1 is Element of bool the carrier of X

X is non empty TopSpace-like almost_discrete extremally_disconnected hereditarily_extremally_disconnected TopStruct

the carrier of X is non empty set

bool the carrier of X is non empty set

X0 is Element of bool the carrier of X

{ (Cl {b

union { (Cl {b

Cl X0 is closed Element of bool the carrier of X

X is non empty TopSpace-like almost_discrete extremally_disconnected hereditarily_extremally_disconnected TopStruct

the carrier of X is non empty set

bool the carrier of X is non empty set

X0 is Element of bool the carrier of X

Z0 is Element of the carrier of X

{Z0} is non empty trivial 1 -element compact Element of bool the carrier of X

Cl {Z0} is closed Element of bool the carrier of X

X0 /\ (Cl {Z0}) is Element of bool the carrier of X

{ (Cl {b

union { (Cl {b

Z0 is set

Z1 is Element of the carrier of X

{Z1} is non empty trivial 1 -element compact Element of bool the carrier of X

Cl {Z1} is closed Element of bool the carrier of X

Z1 is Element of the carrier of X

{Z1} is non empty trivial 1 -element compact Element of bool the carrier of X

Cl {Z1} is closed Element of bool the carrier of X

Z1 is Element of the carrier of X

{Z1} is non empty trivial 1 -element compact Element of bool the carrier of X

Z0 is Element of bool the carrier of X

Z0 is set

Z1 is Element of the carrier of X

{Z1} is non empty trivial 1 -element compact Element of bool the carrier of X

Cl {Z1} is closed Element of bool the carrier of X

X0 /\ (Cl {Z1}) is Element of bool the carrier of X

Z0 /\ (Cl {Z1}) is Element of bool the carrier of X

Z1 is Element of the carrier of X

{Z1} is non empty trivial 1 -element compact Element of bool the carrier of X

Z0 is Element of the carrier of X

{Z0} is non empty trivial 1 -element compact Element of bool the carrier of X

Cl {Z0} is closed Element of bool the carrier of X

X0 /\ (Cl {Z0}) is Element of bool the carrier of X

Z0 is Element of the carrier of X

{Z0} is non empty trivial 1 -element compact Element of bool the carrier of X

X is non empty TopSpace-like almost_discrete extremally_disconnected hereditarily_extremally_disconnected TopStruct

the carrier of X is non empty set

bool the carrier of X is non empty set

X0 is Element of bool the carrier of X

[#] X is non empty non proper open closed dense non boundary Element of bool the carrier of X

Cl X0 is closed Element of bool the carrier of X

([#] X) \ (Cl X0) is Element of bool the carrier of X

{ (Cl {b

Z1 is set

bool the carrier of X is non empty Element of bool (bool the carrier of X)

bool (bool the carrier of X) is non empty set

Z1 is Element of the carrier of X

{Z1} is non empty trivial 1 -element compact Element of bool the carrier of X

Cl {Z1} is closed Element of bool the carrier of X

(Cl X0) ` is open Element of bool the carrier of X

the carrier of X \ (Cl X0) is set

Cl (([#] X) \ (Cl X0)) is closed Element of bool the carrier of X

X0 /\ (([#] X) \ (Cl X0)) is Element of bool the carrier of X

Z1 is Element of bool (bool the carrier of X)

Z1 is Element of bool (bool the carrier of X)

X1 is Element of bool the carrier of X

g is Element of the carrier of X

{g} is non empty trivial 1 -element compact Element of bool the carrier of X

Cl {g} is closed Element of bool the carrier of X

[:Z1, the carrier of X:] is Relation-like set

bool [:Z1, the carrier of X:] is non empty set

X1 is Relation-like Function-like V17(Z1) V21(Z1, the carrier of X) Element of bool [:Z1, the carrier of X:]

X1 .: Z1 is Element of bool the carrier of X

X0 \/ (X1 .: Z1) is Element of bool the carrier of X

g is set

h is set

X1 . h is set

g is Element of the carrier of X

{g} is non empty trivial 1 -element compact Element of bool the carrier of X

Cl {g} is closed Element of bool the carrier of X

(X0 \/ (X1 .: Z1)) /\ (Cl {g}) is Element of bool the carrier of X

(Cl X0) \/ (([#] X) \ (Cl X0)) is Element of bool the carrier of X

X0 /\ (Cl {g}) is Element of bool the carrier of X

h is Element of the carrier of X

{h} is non empty trivial 1 -element compact Element of bool the carrier of X

r is Element of the carrier of X

(X1 .: Z1) /\ (Cl {g}) is Element of bool the carrier of X

(X0 /\ (Cl {g})) \/ {} is set

{r} is non empty trivial 1 -element compact Element of bool the carrier of X

h is Element of the carrier of X

{h} is non empty trivial 1 -element compact Element of bool the carrier of X

X1 . (Cl {g}) is set

h is Element of the carrier of X

x is set

y is Element of the carrier of X

C is set

X1 . C is set

C is Element of bool the carrier of X

w is Element of the carrier of X

{w} is non empty trivial 1 -element compact Element of bool the carrier of X

Cl {w} is closed Element of bool the carrier of X

{y} is non empty trivial 1 -element compact Element of bool the carrier of X

Cl {y} is closed Element of bool the carrier of X

X1 . (Cl {w}) is set

r is Element of the carrier of X

{r} is non empty trivial 1 -element compact Element of bool the carrier of X

h is Element of the carrier of X

{h} is non empty trivial 1 -element compact Element of bool the carrier of X

h is Element of the carrier of X

{h} is non empty trivial 1 -element compact Element of bool the carrier of X

X is non empty TopSpace-like almost_discrete extremally_disconnected hereditarily_extremally_disconnected TopStruct

the carrier of X is non empty set

bool the carrier of X is non empty set

{} X is empty trivial proper Relation-like non-empty empty-yielding Function-like one-to-one constant functional V24() V25() V26() V28() V29() V30() V31() cardinal {} -element open closed boundary nowhere_dense compact Element of bool the carrier of X

Z0 is Element of bool the carrier of X

X is non empty TopSpace-like almost_discrete extremally_disconnected hereditarily_extremally_disconnected TopStruct

X0 is non empty TopSpace-like discrete almost_discrete extremally_disconnected hereditarily_extremally_disconnected SubSpace of X

the carrier of X is non empty set

bool the carrier of X is non empty set

the carrier of X0 is non empty set

Z0 is Element of bool the carrier of X

Z0 is Element of bool the carrier of X

Z1 is non empty strict TopSpace-like almost_discrete extremally_disconnected hereditarily_extremally_disconnected SubSpace of X

the carrier of Z1 is non empty set

X is non empty non trivial TopSpace-like non discrete 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 non trivial set

bool the carrier of X is non empty set

the carrier of X0 is non empty set

Z0 is Element of bool the carrier of X

the topology of X0 is non empty open Element of bool (bool the carrier of X0)

bool the carrier of X0 is non empty set

bool (bool the carrier of X0) is non empty set

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

the topology of X is non empty open Element of bool (bool the carrier of X)

bool (bool the carrier of X) is non empty set

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

X0 is non empty TopSpace-like almost_discrete extremally_disconnected hereditarily_extremally_disconnected SubSpace of X

X is non empty non trivial TopSpace-like non anti-discrete 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 non trivial set

bool the carrier of X is non empty set

the carrier of X0 is non empty set

Z0 is non empty Element of bool the carrier of X

Cl Z0 is closed Element of bool the carrier of X

Z0 is Element of the carrier of X0

{Z0} is non empty trivial 1 -element compact Element of bool the carrier of X0

bool the carrier of X0 is non empty set

Z1 is Element of the carrier of X

{Z1} is non empty trivial proper 1 -element compact Element of bool the carrier of X

Z1 is Element of bool the carrier of X

X1 is Element of the carrier of X

{X1} is non empty trivial proper 1 -element compact Element of bool the carrier of X

Cl Z1 is closed Element of bool the carrier of X

X0 is non empty TopSpace-like almost_discrete extremally_disconnected hereditarily_extremally_disconnected SubSpace of X

X is non empty TopSpace-like almost_discrete extremally_disconnected hereditarily_extremally_disconnected TopStruct

the carrier of X is non empty set

bool the carrier of X is non empty set

X0 is Element of bool the carrier of X

Z0 is non empty strict TopSpace-like almost_discrete extremally_disconnected hereditarily_extremally_disconnected SubSpace of X

the carrier of Z0 is non empty set

X is TopSpace-like discrete almost_discrete TopStruct

the carrier of X is set

X0 is TopSpace-like TopStruct

the carrier of X0 is set

[: the carrier of X, the carrier of X0:] is Relation-like set

bool [: the carrier of X, the carrier of X0:] is non empty set

Z0 is Relation-like Function-like V21( the carrier of X, the carrier of X0) Element of bool [: the carrier of X, the carrier of X0:]

bool the carrier of X0 is non empty set

Z0 is Element of bool the carrier of X0

Z0 " Z0 is Element of bool the carrier of X

bool the carrier of X is non empty set

X is non empty TopSpace-like TopStruct

the carrier of X is non empty set

1TopSp the carrier of X is non empty strict TopSpace-like discrete almost_discrete extremally_disconnected hereditarily_extremally_disconnected TopStruct

bool the carrier of X is non empty Element of bool (bool the carrier of X)

bool the carrier of X is non empty set

bool (bool the carrier of X) is non empty set

[#] (bool the carrier of X) is non empty non proper Element of bool (bool the carrier of X)

bool (bool the carrier of X) is non empty set

TopStruct(# the carrier of X,([#] (bool the carrier of X)) #) is non empty strict TopStruct

the carrier of (1TopSp the carrier of X) is non empty set

[: the carrier of X, the carrier of (1TopSp the carrier of X):] is non empty Relation-like set

bool [: the carrier of X, the carrier of (1TopSp the carrier of X):] is non empty set

id the carrier of X is non empty Relation-like the carrier of X -defined the carrier of X -valued Function-like one-to-one V17( the carrier of X) V21( the carrier of X, the carrier of X) Element of bool [: the carrier of X, the carrier of X:]

[: the carrier of X, the carrier of X:] is non empty Relation-like set

bool [: the carrier of X, the carrier of X:] is non empty set

Z0 is non empty Relation-like Function-like V17( the carrier of X) V21( the carrier of X, the carrier of (1TopSp the carrier of X)) Element of bool [: the carrier of X, the carrier of (1TopSp the carrier of X):]

Z0 is Element of bool the carrier of X

bool the carrier of (1TopSp the carrier of X) is non empty set

Z1 is Element of bool the carrier of (1TopSp the carrier of X)

Z0 " Z1 is Element of bool the carrier of X

X is non empty TopSpace-like TopStruct

the carrier of X is non empty set

X0 is non empty TopSpace-like anti-discrete almost_discrete extremally_disconnected hereditarily_extremally_disconnected TopStruct

the carrier of X0 is non empty set

[: the carrier of X, the carrier of X0:] is non empty Relation-like set

bool [: the carrier of X, the carrier of X0:] is non empty set

Z0 is non empty Relation-like Function-like V17( the carrier of X) V21( the carrier of X, the carrier of X0) Element of bool [: the carrier of X, the carrier of X0:]

bool the carrier of X0 is non empty set

Z0 is Element of bool the carrier of X0

Z0 " Z0 is Element of bool the carrier of X

bool the carrier of X is non empty set

{} X is empty trivial proper Relation-like non-empty empty-yielding Function-like one-to-one constant functional V24() V25() V26() V28() V29() V30() V31() cardinal {} -element open closed boundary nowhere_dense compact Element of bool the carrier of X

[#] X0 is non empty non proper open closed dense non boundary Element of bool the carrier of X0

Z0 " Z0 is Element of bool the carrier of X

bool the carrier of X is non empty set

[#] X is non empty non proper open closed dense non boundary Element of bool the carrier of X

Z0 " Z0 is Element of bool the carrier of X

bool the carrier of X is non empty set

Z0 " Z0 is Element of bool the carrier of X

bool the carrier of X is non empty set

X is non empty TopSpace-like TopStruct

the carrier of X is non empty set

ADTS the carrier of X is non empty strict TopSpace-like anti-discrete almost_discrete extremally_disconnected hereditarily_extremally_disconnected TopStruct

cobool the carrier of X is non empty Element of bool (bool the carrier of X)

bool the carrier of X is non empty set

bool (bool the carrier of X) is non empty set

TopStruct(# the carrier of X,(cobool the carrier of X) #) is non empty strict TopStruct

the carrier of (ADTS the carrier of X) is non empty set

[: the carrier of (ADTS the carrier of X), the carrier of X:] is non empty Relation-like set

bool [: the carrier of (ADTS the carrier of X), the carrier of X:] is non empty set

id the carrier of X is non empty Relation-like the carrier of X -defined the carrier of X -valued Function-like one-to-one V17( the carrier of X) V21( the carrier of X, the carrier of X) Element of bool [: the carrier of X, the carrier of X:]

[: the carrier of X, the carrier of X:] is non empty Relation-like set

bool [: the carrier of X, the carrier of X:] is non empty set

Z0 is non empty Relation-like Function-like V17( the carrier of (ADTS the carrier of X)) V21( the carrier of (ADTS the carrier of X), the carrier of X) Element of bool [: the carrier of (ADTS the carrier of X), the carrier of X:]

Z0 is Element of bool the carrier of X

bool the carrier of (ADTS the carrier of X) is non empty set

Z0 " Z0 is Element of bool the carrier of (ADTS the carrier of X)

Z1 is Element of bool the carrier of (ADTS the carrier of X)

X is non empty TopSpace-like discrete almost_discrete extremally_disconnected hereditarily_extremally_disconnected TopStruct

the carrier of X is non empty set

X0 is non empty TopSpace-like closed open discrete almost_discrete extremally_disconnected hereditarily_extremally_disconnected SubSpace of X

the carrier of X0 is non empty set

[: the carrier of X, the carrier of X0:] is non empty Relation-like set

bool [: the carrier of X, the carrier of X0:] is non empty set

bool the carrier of X is non empty set

Z0 is Element of bool the carrier of X

Z0 is Element of the carrier of X

Z0 is non empty Relation-like Function-like V17( the carrier of X) V21( the carrier of X, the carrier of X0) Element of bool [: the carrier of X, the carrier of X0:]

Z1 is non empty Relation-like Function-like V17( the carrier of X) V21( the carrier of X, the carrier of X0) continuous Element of bool [: the carrier of X, the carrier of X0:]

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 SubSpace of X

the carrier of X is non empty set

the carrier of X0 is non empty set

[: the carrier of X, the carrier of X0:] is non empty Relation-like set

bool [: the carrier of X, the carrier of X0:] is non empty set

Z0 is non empty Relation-like Function-like V17( the carrier of X) V21( the carrier of X, the carrier of X0) continuous Element of bool [: the carrier of X, the carrier of X0:]

X is non empty TopSpace-like almost_discrete extremally_disconnected hereditarily_extremally_disconnected TopStruct

the carrier of X is non empty set

X0 is non empty TopSpace-like discrete almost_discrete extremally_disconnected hereditarily_extremally_disconnected (X) SubSpace of X

the carrier of X0 is non empty set

[: the carrier of X, the carrier of X0:] is non empty Relation-like set

bool [: the carrier of X, the carrier of X0:] is non empty set

bool the carrier of X is non empty set

Z0 is Element of bool the carrier of X

Z0 is Element of the carrier of X

{Z0} is non empty trivial 1 -element compact Element of bool the carrier of X

Cl {Z0} is closed Element of bool the carrier of X

Z0 /\ (Cl {Z0}) is Element of bool the carrier of X

Z1 is Element of the carrier of X

{Z1} is non empty trivial 1 -element compact Element of bool the carrier of X

Z1 is Element of the carrier of X0

{Z1} is non empty trivial 1 -element compact Element of bool the carrier of X0

bool the carrier of X0 is non empty set

Z0 is non empty Relation-like Function-like V17( the carrier of X) V21( the carrier of X, the carrier of X0) Element of bool [: the carrier of X, the carrier of X0:]

bool the carrier of X0 is non empty set

Z1 is Element of bool the carrier of X0

Z0 " Z1 is Element of bool the carrier of X

Z1 is Element of bool the carrier of X

{ (Cl {b

g is set

g is Element of the carrier of X

Z0 . g is Element of the carrier of X0

h is Element of the carrier of X

{h} is non empty trivial 1 -element compact Element of bool the carrier of X

Cl {h} is closed Element of bool the carrier of X

union { (Cl {b

{g} is non empty trivial 1 -element compact Element of bool the carrier of X

Cl {g} is closed Element of bool the carrier of X

Z0 /\ (Cl {g}) is Element of bool the carrier of X

g is set

g is Element of the carrier of X

{g} is non empty trivial 1 -element compact Element of bool the carrier of X

Cl {g} is closed Element of bool the carrier of X

h is set

r is Element of the carrier of X

{r} is non empty trivial 1 -element compact Element of bool the carrier of X

Cl {r} is closed Element of bool the carrier of X

Z0 /\ (Cl {r}) is Element of bool the carrier of X

Z0 . r is Element of the carrier of X0

{(Z0 . r)} is non empty trivial 1 -element compact Element of bool the carrier of X0

Z0 /\ (Cl {g}) is Element of bool the carrier of X

Z0 . h is set

Cl Z1 is closed Element of bool the carrier of X

Z1 is non empty Relation-like Function-like V17( the carrier of X) V21( the carrier of X, the carrier of X0) continuous Element of bool [: the carrier of X, the carrier of X0:]

Z1 is Element of the carrier of X

Z1 . Z1 is Element of the carrier of X0

{Z1} is non empty trivial 1 -element compact Element of bool the carrier of X

Cl {Z1} is closed Element of bool the carrier of X

Z0 /\ (Cl {Z1}) is Element of bool the carrier of X

{(Z1 . Z1)} is non empty trivial 1 -element compact Element of bool the carrier of X0

X is non empty TopSpace-like almost_discrete extremally_disconnected hereditarily_extremally_disconnected TopStruct

X0 is non empty TopSpace-like discrete almost_discrete extremally_disconnected hereditarily_extremally_disconnected (X) SubSpace of X

the carrier of X is non empty set

the carrier of X0 is non empty set

[: the carrier of X, the carrier of X0:] is non empty Relation-like set

bool [: the carrier of X, the carrier of X0:] is non empty set

Z0 is non empty Relation-like Function-like V17( the carrier of X) V21( the carrier of X, the carrier of X0) continuous Element of bool [: the carrier of X, the carrier of X0:]

X is non empty TopSpace-like almost_discrete extremally_disconnected hereditarily_extremally_disconnected TopStruct

the carrier of X is non empty set

X0 is non empty TopSpace-like discrete almost_discrete extremally_disconnected hereditarily_extremally_disconnected (X) SubSpace of X

the carrier of X0 is non empty set

[: the carrier of X, the carrier of X0:] is non empty Relation-like set

bool [: the carrier of X, the carrier of X0:] is non empty set

Z0 is non empty Relation-like Function-like V17( the carrier of X) V21( the carrier of X, the carrier of X0) continuous Element of bool [: the carrier of X, the carrier of X0:]

Z0 is Element of the carrier of X0

{Z0} is non empty trivial 1 -element compact Element of bool the carrier of X0

bool the carrier of X0 is non empty set

Z0 " {Z0} is Element of bool the carrier of X

bool the carrier of X is non empty set

Z1 is Element of the carrier of X

{Z1} is non empty trivial 1 -element compact Element of bool the carrier of X

Cl {Z1} is closed Element of bool the carrier of X

Z0 . Z1 is Element of the carrier of X0

X is non empty TopSpace-like almost_discrete extremally_disconnected hereditarily_extremally_disconnected TopStruct

the carrier of X is non empty set

bool the carrier of X is non empty set

X0 is non empty TopSpace-like discrete almost_discrete extremally_disconnected hereditarily_extremally_disconnected (X) SubSpace of X

the carrier of X0 is non empty set

[: the carrier of X, the