:: 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₁() is non empty TopStruct
the carrier of F₁() is non empty set
bool the carrier of F₁() is non empty set
bool (bool the carrier of F₁()) is non empty set
F₂() is Element of bool (bool the carrier of F₁())
[:F₂(), the carrier of F₁():] is Relation-like set
bool [:F₂(), the carrier of F₁():] is non empty set
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₂()) V21(F₂(), the carrier of F₁()) Element of bool [:F₂(), the carrier of 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₁}) where b₁ is Element of the carrier of X : b₁ in X0 } is set
union { (Cl {b₁}) where b₁ is Element of the carrier of X : b₁ in X0 } is set
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₁}) where b₁ is Element of the carrier of X : b₁ in X0 } is set
union { (Cl {b₁}) where b₁ is Element of the carrier of X : b₁ in X0 } is set
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<sub>1</sub>}) where b<sub>1</sub> is Element of the carrier of X : b<sub>1</sub> in X0 } is set
union { (Cl {b<sub>1</sub>}) where b<sub>1</sub> is Element of the carrier of X : b<sub>1</sub> in X0 } is set
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<sub>1</sub>}) where b<sub>1</sub> is Element of the carrier of X : b<sub>1</sub> in X0 } is set
union { (Cl {b<sub>1</sub>}) where b<sub>1</sub> is Element of the carrier of X : b<sub>1</sub> in X0 } is set
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<sub>1</sub>}) where b<sub>1</sub> is Element of the carrier of X : b<sub>1</sub> in ([#] X) \ (Cl X0) } is set
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₁}) where b₁ is Element of the carrier of X : b₁ in Z1 } is set
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₁}) where b₁ is Element of the carrier of X : b₁ in Z1 } is set
{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 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 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 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
Z0 /\ (Cl {Z1}) is Element of bool the carrier of X
Z0 . Z1 is Element of the carrier of X0
{(Z0 . Z1)} is non empty trivial 1 -element compact Element of bool the carrier of X0
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
X1 is Element of the carrier of X0
{X1} is non empty trivial 1 -element compact Element of bool the carrier of X0
Z0 " {X1} is Element of bool the carrier of X
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 Z1 is closed Element of bool the carrier of X
{ (Cl {b₁}) where b₁ is Element of the carrier of X : b₁ in Z1 } is set
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₁}) where b₁ is Element of the carrier of X : b₁ in Z1 } is set
{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
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
Z1 is Element of the carrier of X
{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 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
X0 is non empty TopSpace-like 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
Z0 is non empty strict TopSpace-like almost_discrete extremally_disconnected hereditarily_extremally_disconnected SubSpace of X
Z0 is non empty strict TopSpace-like discrete almost_discrete extremally_disconnected hereditarily_extremally_disconnected (X) SubSpace of X
Z1 is non empty TopSpace-like TopStruct
Z1 is non empty TopSpace-like discrete almost_discrete extremally_disconnected hereditarily_extremally_disconnected TopStruct
the carrier of Z1 is non empty set
X1 is non empty TopSpace-like closed open discrete almost_discrete extremally_disconnected hereditarily_extremally_disconnected SubSpace of Z1
the carrier of X1 is non empty set
[: the carrier of Z1, the carrier of X1:] is non empty Relation-like set
bool [: the carrier of Z1, the carrier of X1:] is non empty set
g is non empty Relation-like Function-like V17( the carrier of Z1) V21( the carrier of Z1, the carrier of X1) continuous Element of bool [: the carrier of Z1, the carrier of X1:]
the carrier of Z0 is non empty set
[: the carrier of Z0, the carrier of X0:] is non empty Relation-like set
bool [: the carrier of Z0, the carrier of X0:] is non empty set
[: the carrier of X, the carrier of Z0:] is non empty Relation-like set
bool [: the carrier of X, the carrier of Z0:] is non empty set
h is non empty Relation-like Function-like V17( the carrier of X) V21( the carrier of X, the carrier of Z0) continuous Element of bool [: the carrier of X, the carrier of Z0:]
g is non empty Relation-like Function-like V17( the carrier of Z0) V21( the carrier of Z0, the carrier of X0) continuous Element of bool [: the carrier of Z0, the carrier of X0:]
g * h is non empty Relation-like Function-like V17( the carrier of X) V17( the carrier of X) V21( the carrier of X, the carrier of X0) V21( the carrier of X, the carrier of X0) continuous Element of bool [: the carrier of X, the carrier of X0:]
r 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 Element of the carrier of X
r . x is Element of the carrier of X0
y is Element of the carrier of Z1
g . y is set
h . x is Element of the carrier of Z0
g . (h . x) is Element of 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 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:]