{} is empty finite V28() set
the empty finite V28() set is empty finite V28() set
1 is non empty set
{{},1} is non empty finite set
K137() is set
bool K137() is non empty set
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
bool the carrier of T is non empty set
Z is Element of bool the carrier of T
X is Element of the carrier of T
Z ` is Element of bool the carrier of T
the carrier of T \ Z is set
X is Element of the carrier of T
Z is Element of bool the carrier of T
Z ` is Element of bool the carrier of T
the carrier of T \ Z is set
[#] T is non empty non proper open closed Element of bool the carrier of T
F is non empty non proper open closed Element of bool the carrier of T
{} T is empty proper finite V28() open closed Element of bool the carrier of T
FF is empty proper finite V28() open closed Element of bool the carrier of T
X is Element of bool the carrier of T
Z is Element of bool the carrier of T
X is Element of bool the carrier of T
Z is Element of bool the carrier of T
{} T is empty proper finite V28() open closed Element of bool the carrier of T
F is empty proper finite V28() open closed Element of bool the carrier of T
[#] T is non empty non proper open closed Element of bool the carrier of T
FF is non empty non proper open closed Element of bool the carrier of T
[#] T is non empty non proper open closed Element of bool the carrier of T
F is non empty non proper open closed Element of bool the carrier of T
{} T is empty proper finite V28() open closed Element of bool the carrier of T
FF is empty proper finite V28() open closed Element of bool the carrier of T
T is TopStruct
the carrier of T is set
bool the carrier of T is non empty set
T is TopStruct
the carrier of T is set
bool the carrier of T is non empty set
bool (bool the carrier of T) is non empty set
Z is Element of bool the carrier of T
X is Element of bool (bool the carrier of T)
union X is Element of bool the carrier of T
F is Element of bool (bool the carrier of T)
T is TopStruct
[#] T is non proper Element of bool the carrier of T
the carrier of T is set
bool the carrier of T is non empty set
bool (bool the carrier of T) is non empty set
X is Element of bool (bool the carrier of T)
Z is Element of bool (bool the carrier of T)
bool (bool the carrier of T) is non empty set
X is Element of bool (bool the carrier of T)
Z is Element of bool (bool the carrier of T)
T is TopStruct
the carrier of T is set
bool the carrier of T is non empty set
X is SubSpace of T
[#] X is non proper Element of bool the carrier of X
the carrier of X is set
bool the carrier of X is non empty set
Z is Element of bool the carrier of T
[#] T is non proper Element of bool the carrier of T
F is Element of bool the carrier of T
Z /\ F is Element of bool the carrier of T
FF is Element of bool the carrier of X
bool (bool the carrier of X) is non empty set
G is Element of bool (bool the carrier of X)
bool (bool the carrier of T) is non empty set
g is Element of bool (bool the carrier of T)
union G is Element of bool the carrier of X
T | F is strict SubSpace of T
the carrier of (T | F) is set
g | F is Element of bool (bool the carrier of (T | F))
bool the carrier of (T | F) is non empty set
bool (bool the carrier of (T | F)) is non empty set
union (g | F) is Element of bool the carrier of (T | F)
union g is Element of bool the carrier of T
h is Element of bool (bool the carrier of T)
h | F is Element of bool (bool the carrier of (T | F))
[#] (T | F) is non proper Element of bool the carrier of (T | F)
bool ([#] (T | F)) is non empty Element of bool (bool ([#] (T | F)))
bool ([#] (T | F)) is non empty set
bool (bool ([#] (T | F))) is non empty set
h is Element of bool (bool the carrier of X)
union h is Element of bool the carrier of T
union h is Element of bool the carrier of X
FF is Element of bool the carrier of X
bool (bool the carrier of T) is non empty set
G is Element of bool (bool the carrier of T)
G | F is Element of bool (bool the carrier of (T | F))
T | F is strict SubSpace of T
the carrier of (T | F) is set
bool the carrier of (T | F) is non empty set
bool (bool the carrier of (T | F)) is non empty set
g is Relation-like Function-like set
dom g is set
rng g is set
[#] (T | F) is non proper Element of bool the carrier of (T | F)
bool ([#] (T | F)) is non empty Element of bool (bool ([#] (T | F)))
bool ([#] (T | F)) is non empty set
bool (bool ([#] (T | F))) is non empty set
bool (bool the carrier of X) is non empty set
h is Element of bool (bool the carrier of X)
h is Element of bool the carrier of X
P is Element of bool the carrier of (T | F)
P1 is Element of bool the carrier of T
P1 /\ F is Element of bool the carrier of T
the topology of T is Element of bool (bool the carrier of T)
the topology of X is Element of bool (bool the carrier of X)
union G is Element of bool the carrier of T
union h is Element of bool the carrier of X
h is Element of bool (bool the carrier of X)
P is set
g .: P is set
P1 is Element of bool (bool the carrier of T)
union P1 is Element of bool the carrier of T
P2 is set
union h is Element of bool the carrier of X
x is set
x is set
g . x is set
D is Element of bool the carrier of T
D /\ F is Element of bool the carrier of T
T is TopStruct
the carrier of T is set
bool the carrier of T is non empty set
X is Element of bool the carrier of T
T | X is strict SubSpace of T
[#] (T | X) is non proper Element of bool the carrier of (T | X)
the carrier of (T | X) is set
bool the carrier of (T | X) is non empty set
Z is non empty TopSpace-like TopStruct
the carrier of Z is non empty set
bool the carrier of Z is non empty set
F is non empty Element of bool the carrier of Z
Z | F is non empty strict TopSpace-like SubSpace of Z
[#] (Z | F) is non empty non proper open closed Element of bool the carrier of (Z | F)
the carrier of (Z | F) is non empty set
bool the carrier of (Z | F) is non empty set
FF is Element of bool the carrier of (T | X)
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
bool the carrier of T is non empty set
bool (bool the carrier of T) is non empty set
X is Element of bool (bool the carrier of T)
meet X is Element of bool the carrier of T
COMPLEMENT X is Element of bool (bool the carrier of T)
union (COMPLEMENT X) is Element of bool the carrier of T
(meet X) ` is Element of bool the carrier of T
the carrier of T \ (meet X) is set
[#] T is non empty non proper open closed Element of bool the carrier of T
Z is Element of bool (bool the carrier of T)
F is Element of bool (bool the carrier of T)
COMPLEMENT F is Element of bool (bool the carrier of T)
G is set
c7 is Element of bool the carrier of T
c7 ` is Element of bool the carrier of T
the carrier of T \ c7 is set
(c7 `) ` is Element of bool the carrier of T
the carrier of T \ (c7 `) is set
meet (COMPLEMENT F) is Element of bool the carrier of T
union F is Element of bool the carrier of T
(union F) ` is Element of bool the carrier of T
the carrier of T \ (union F) is set
([#] T) \ ([#] T) is Element of bool the carrier of T
X is Element of bool (bool the carrier of T)
COMPLEMENT X is Element of bool (bool the carrier of T)
Z is Element of bool (bool the carrier of T)
meet Z is Element of bool the carrier of T
union X is Element of bool the carrier of T
(union X) ` is Element of bool the carrier of T
the carrier of T \ (union X) is set
[#] T is non empty non proper open closed Element of bool the carrier of T
([#] T) \ ([#] T) is Element of bool the carrier of T
F is set
meet F is set
FF is Element of bool (bool the carrier of T)
COMPLEMENT FF is Element of bool (bool the carrier of T)
G is Element of bool (bool the carrier of T)
c7 is set
g is Element of bool the carrier of T
g ` is Element of bool the carrier of T
the carrier of T \ g is set
(g `) ` is Element of bool the carrier of T
the carrier of T \ (g `) is set
union G is Element of bool the carrier of T
meet FF is Element of bool the carrier of T
(meet FF) ` is Element of bool the carrier of T
the carrier of T \ (meet FF) is set
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
bool the carrier of T is non empty set
bool (bool the carrier of T) is non empty set
X is Element of bool (bool the carrier of T)
meet X is Element of bool the carrier of T
Z is set
meet Z is set
F is Element of bool (bool the carrier of T)
meet F is Element of bool the carrier of T
X is Element of bool (bool the carrier of T)
meet X is Element of bool the carrier of T
Z is Element of bool (bool the carrier of T)
meet Z is Element of bool the carrier of T
T is TopSpace-like TopStruct
the carrier of T is set
bool the carrier of T is non empty set
X is Element of bool the carrier of T
X ` is Element of bool the carrier of T
the carrier of T \ X is set
the Element of X is Element of X
F is Element of the carrier of T
the topology of T is non empty Element of bool (bool the carrier of T)
bool (bool the carrier of T) is non empty set
FF is set
G is Element of the carrier of T
c7 is Element of bool the carrier of T
g is Element of bool the carrier of T
h is set
h is set
c7 /\ g is Element of bool the carrier of T
FF is Relation-like Function-like set
dom FF is set
G is Relation-like Function-like set
dom G is set
G .: X is set
bool the carrier of T is non empty Element of bool (bool the carrier of T)
c7 is set
g is set
G . g is set
FF . g is set
h is Element of bool the carrier of T
h is Element of bool the carrier of T
h /\ h is Element of bool the carrier of T
c7 is Element of bool (bool the carrier of T)
g is Element of bool the carrier of T
h is set
G . h is set
FF . h is set
h is Element of bool the carrier of T
P is Element of bool the carrier of T
h /\ P is Element of bool the carrier of T
union c7 is Element of bool the carrier of T
g is set
FF . g is set
G . g is set
h is Element of bool the carrier of T
h is Element of bool the carrier of T
h /\ h is Element of bool the carrier of T
g is Element of bool (bool the carrier of T)
rng G is set
h is set
G .: h is set
FF .: h is set
h is set
P is set
FF . P is set
G . P is set
P1 is Element of bool the carrier of T
P2 is Element of bool the carrier of T
P1 /\ P2 is Element of bool the carrier of T
h is Element of bool (bool the carrier of T)
meet h is Element of bool the carrier of T
P is Element of bool the carrier of T
union g is Element of bool the carrier of T
P1 is Element of bool the carrier of T
P2 is Element of bool the carrier of T
x is set
FF . x is set
G . x is set
x is Element of bool the carrier of T
D is Element of bool the carrier of T
x /\ D is Element of bool the carrier of T
P2 is set
x is Element of bool the carrier of T
x is set
FF . x is set
G . x is set
D is Element of bool the carrier of T
z is Element of bool the carrier of T
D /\ z is Element of bool the carrier of T
P2 is set
x is Element of bool the carrier of T
x is set
G . x is set
FF . x is set
D is Element of bool the carrier of T
z is Element of bool the carrier of T
D /\ z is Element of bool the carrier of T
P /\ P1 is Element of bool the carrier of T
(meet h) /\ (union g) is Element of bool the carrier of T
the Element of (meet h) /\ (union g) is Element of (meet h) /\ (union g)
z is set
P is set
G . P is set
FF . P is set
Q is Element of bool the carrier of T
QS is Element of bool the carrier of T
Q /\ QS is Element of bool the carrier of T
T is TopSpace-like TopStruct
the carrier of T is set
bool the carrier of T is non empty set
X is Element of bool the carrier of T
Z is set
X ` is Element of bool the carrier of T
the carrier of T \ X is set
F is Element of the carrier of T
FF is Element of bool the carrier of T
G is Element of bool the carrier of T
c7 is Element of bool the carrier of T
G ` is Element of bool the carrier of T
the carrier of T \ G is set
(G `) ` is Element of bool the carrier of T
the carrier of T \ (G `) is set
F is Element of bool the carrier of T
T is TopStruct
the carrier of T is set
bool the carrier of T is non empty set
X is Element of bool the carrier of T
bool (bool the carrier of T) is non empty set
X ` is Element of bool the carrier of T
the carrier of T \ X is set
{(X `)} is non empty finite Element of bool (bool the carrier of T)
F is Element of bool (bool the carrier of T)
Z is Element of bool (bool the carrier of T)
F \/ Z is Element of bool (bool the carrier of T)
G is Element of bool the carrier of T
F \/ {(X `)} is non empty Element of bool (bool the carrier of T)
(F \/ {(X `)}) \ {(X `)} is Element of bool (bool the carrier of T)
F \ {(X `)} is Element of bool (bool the carrier of T)
union F is Element of bool the carrier of T
X \/ (X `) is Element of bool the carrier of T
(union F) \/ (X `) is Element of bool the carrier of T
[#] T is non proper Element of bool the carrier of T
union {(X `)} is Element of bool the carrier of T
(union F) \/ (union {(X `)}) is Element of bool the carrier of T
union (F \/ {(X `)}) is Element of bool the carrier of T
c7 is Element of bool (bool the carrier of T)
c7 \ Z is Element of bool (bool the carrier of T)
g is Element of bool (bool the carrier of T)
union c7 is Element of bool the carrier of T
G is Element of bool (bool the carrier of T)
union G is Element of bool the carrier of T
(union c7) \ (union G) is Element of bool the carrier of T
([#] T) \ (union {(X `)}) is Element of bool the carrier of T
(X `) ` is Element of bool the carrier of T
the carrier of T \ (X `) is set
union g is Element of bool the carrier of T
T is TopSpace-like TopStruct
the carrier of T is set
bool the carrier of T is non empty set
X is Element of bool the carrier of T
Z is Element of bool the carrier of T
T | X is strict TopSpace-like SubSpace of T
the carrier of (T | X) is set
bool the carrier of (T | X) is non empty set
F is Element of bool the carrier of (T | X)
[#] (T | X) is non proper open closed Element of bool the carrier of (T | X)
T is TopStruct
the carrier of T is set
bool the carrier of T is non empty set
X is Element of bool the carrier of T
Z is Element of bool the carrier of T
X \/ Z is Element of bool the carrier of T
bool (bool the carrier of T) is non empty set
F is Element of bool (bool the carrier of T)
union F is Element of bool the carrier of T
FF is Element of bool (bool the carrier of T)
union FF is Element of bool the carrier of T
G is Element of bool (bool the carrier of T)
G \/ FF is Element of bool (bool the carrier of T)
c7 is Element of bool (bool the carrier of T)
union G is Element of bool the carrier of T
(union G) \/ (union FF) is Element of bool the carrier of T
union (G \/ FF) is Element of bool the carrier of T
T is TopSpace-like TopStruct
the carrier of T is set
bool the carrier of T is non empty set
X is Element of bool the carrier of T
Z is Element of bool the carrier of T
X /\ Z is Element of bool the carrier of T
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
bool the carrier of T is non empty set
X is Element of the carrier of T
Z is Element of bool the carrier of T
Z ` is Element of bool the carrier of T
the carrier of T \ Z is set
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
bool the carrier of T is non empty set
X is Element of bool the carrier of T
Z is Element of bool the carrier of T
X /\ Z is Element of bool the carrier of T
the topology of T is non empty Element of bool (bool the carrier of T)
bool (bool the carrier of T) is non empty set
F is set
FF is Element of the carrier of T
Z ` is Element of bool the carrier of T
the carrier of T \ Z is set
G is Element of bool the carrier of T
c7 is Element of bool the carrier of T
g is set
h is set
G /\ c7 is Element of bool the carrier of T
F is Relation-like Function-like set
dom F is set
FF is Relation-like Function-like set
dom FF is set
F .: X is set
bool the carrier of T is non empty Element of bool (bool the carrier of T)
G is set
c7 is set
F . c7 is set
FF . c7 is set
g is Element of bool the carrier of T
h is Element of bool the carrier of T
g /\ h is Element of bool the carrier of T
G is Element of bool (bool the carrier of T)
union G is Element of bool the carrier of T
c7 is set
F . c7 is set
FF . c7 is set
g is Element of bool the carrier of T
h is Element of bool the carrier of T
g /\ h is Element of bool the carrier of T
c7 is Element of bool the carrier of T
g is set
F . g is set
FF . g is set
h is Element of bool the carrier of T
h is Element of bool the carrier of T
h /\ h is Element of bool the carrier of T
c7 is Element of bool (bool the carrier of T)
the Element of X is Element of X
union c7 is Element of bool the carrier of T
h is set
rng F is set
h is set
F .: h is set
FF .: h is set
P is set
P1 is set
FF . P1 is set
F . P1 is set
P2 is Element of bool the carrier of T
x is Element of bool the carrier of T
P2 /\ x is Element of bool the carrier of T
P1 is set
F . P1 is set
P is Element of bool (bool the carrier of T)
P2 is set
x is Element of bool the carrier of T
x is set
FF . x is set
F . x is set
D is Element of bool the carrier of T
z is Element of bool the carrier of T
D /\ z is Element of bool the carrier of T
P2 is Element of bool the carrier of T
meet P is Element of bool the carrier of T
x is Element of bool the carrier of T
x is Element of bool the carrier of T
D is set
FF . D is set
F . D is set
z is Element of bool the carrier of T
P is Element of bool the carrier of T
z /\ P is Element of bool the carrier of T
FF . P1 is set
x is Element of bool the carrier of T
D is Element of bool the carrier of T
x /\ D is Element of bool the carrier of T
P2 /\ x is Element of bool the carrier of T
(union c7) /\ (meet P) is Element of bool the carrier of T
the Element of (union c7) /\ (meet P) is Element of (union c7) /\ (meet P)
D is set
z is set
F . z is set
FF . z is set
P is Element of bool the carrier of T
Q is Element of bool the carrier of T
P /\ Q is Element of bool the carrier of T
T is TopStruct
the carrier of T is set
X is non empty TopStruct
the carrier of X is non empty set
[: the carrier of T, the carrier of X:] is set
bool [: the carrier of T, the carrier of X:] is non empty set
[#] X is non empty non proper Element of bool the carrier of X
bool the carrier of X is non empty set
Z is Relation-like the carrier of T -defined the carrier of X -valued Function-like V21( the carrier of T, the carrier of X) Element of bool [: the carrier of T, the carrier of X:]
rng Z is Element of bool the carrier of X
[#] T is non proper Element of bool the carrier of T
bool the carrier of T is non empty set
dom Z is Element of bool the carrier of T
Z .: ([#] T) is Element of bool the carrier of X
Z " (Z .: ([#] T)) is Element of bool the carrier of T
bool (bool the carrier of X) is non empty set
F is Element of bool (bool the carrier of X)
bool (bool the carrier of T) is non empty set
" Z is Relation-like Function-like set
(" Z) .: F is set
G is Element of bool (bool the carrier of T)
union G is Element of bool the carrier of T
union F is Element of bool the carrier of X
Z " (union F) is Element of bool the carrier of T
Z " (rng Z) is Element of bool the carrier of T
Z .: (dom Z) is Element of bool the carrier of X
Z " (Z .: (dom Z)) is Element of bool the carrier of T
.: Z is Relation-like bool the carrier of T -defined bool the carrier of X -valued Function-like V21( bool the carrier of T, bool the carrier of X) Element of bool [:(bool the carrier of T),(bool the carrier of X):]
[:(bool the carrier of T),(bool the carrier of X):] is non empty set
bool [:(bool the carrier of T),(bool the carrier of X):] is non empty set
(.: Z) " F is Element of bool (bool the carrier of T)
(.: Z) .: ((.: Z) " F) is Element of bool (bool the carrier of X)
(.: Z) .: ((" Z) .: F) is Element of bool (bool the carrier of X)
(.: Z) .: G is Element of bool (bool the carrier of X)
c7 is Element of bool (bool the carrier of T)
(.: Z) .: c7 is Element of bool (bool the carrier of X)
g is Element of bool (bool the carrier of X)
union g is Element of bool the carrier of X
union c7 is Element of bool the carrier of T
Z .: (union c7) is Element of bool the carrier of X
T is TopStruct
the carrier of T is set
bool the carrier of T is non empty set
X is Element of bool the carrier of T
Z is non empty TopStruct
the carrier of Z is non empty set
[: the carrier of T, the carrier of Z:] is set
bool [: the carrier of T, the carrier of Z:] is non empty set
[#] Z is non empty non proper Element of bool the carrier of Z
bool the carrier of Z is non empty set
F is Relation-like the carrier of T -defined the carrier of Z -valued Function-like V21( the carrier of T, the carrier of Z) Element of bool [: the carrier of T, the carrier of Z:]
rng F is Element of bool the carrier of Z
F .: X is Element of bool the carrier of Z
bool (bool the carrier of Z) is non empty set
FF is Element of bool (bool the carrier of Z)
bool (bool the carrier of T) is non empty set
" F is Relation-like Function-like set
(" F) .: FF is set
union FF is Element of bool the carrier of Z
F " (F .: X) is Element of bool the carrier of T
F " (union FF) is Element of bool the carrier of T
[#] T is non proper Element of bool the carrier of T
dom F is Element of bool the carrier of T
G is Element of bool (bool the carrier of T)
union G is Element of bool the carrier of T
c7 is Element of bool (bool the carrier of T)
.: F is Relation-like bool the carrier of T -defined bool the carrier of Z -valued Function-like V21( bool the carrier of T, bool the carrier of Z) Element of bool [:(bool the carrier of T),(bool the carrier of Z):]
[:(bool the carrier of T),(bool the carrier of Z):] is non empty set
bool [:(bool the carrier of T),(bool the carrier of Z):] is non empty set
(.: F) .: c7 is Element of bool (bool the carrier of Z)
g is Element of bool (bool the carrier of Z)
(.: F) " FF is Element of bool (bool the carrier of T)
(.: F) .: ((.: F) " FF) is Element of bool (bool the carrier of Z)
(.: F) .: ((" F) .: FF) is Element of bool (bool the carrier of Z)
(.: F) .: G is Element of bool (bool the carrier of Z)
union c7 is Element of bool the carrier of T
union g is Element of bool the carrier of Z
F .: (union c7) is Element of bool the carrier of Z
T is TopSpace-like TopStruct
the carrier of T is set
bool the carrier of T is non empty set
X is non empty TopSpace-like TopStruct
the carrier of X is non empty set
[: the carrier of T, the carrier of X:] is set
bool [: the carrier of T, the carrier of X:] is non empty set
[#] X is non empty non proper open closed Element of bool the carrier of X
bool the carrier of X is non empty set
Z is Relation-like the carrier of T -defined the carrier of X -valued Function-like V21( the carrier of T, the carrier of X) Element of bool [: the carrier of T, the carrier of X:]
rng Z is Element of bool the carrier of X
F is Element of bool the carrier of T
Z .: F is Element of bool the carrier of X
T is TopSpace-like TopStruct
the carrier of T is set
[#] T is non proper open closed Element of bool the carrier of T
bool the carrier of T is non empty set
X is non empty TopSpace-like TopStruct
the carrier of X is non empty set
[: the carrier of T, the carrier of X:] is set
bool [: the carrier of T, the carrier of X:] is non empty set
[#] X is non empty non proper open closed Element of bool the carrier of X
bool the carrier of X is non empty set
Z is Relation-like the carrier of T -defined the carrier of X -valued Function-like V21( the carrier of T, the carrier of X) Element of bool [: the carrier of T, the carrier of X:]
dom Z is Element of bool the carrier of T
rng Z is Element of bool the carrier of X
F is Element of bool the carrier of T
Z .: F is Element of bool the carrier of X
Z " (Z .: F) is Element of bool the carrier of T
T is set
bool T is non empty Element of bool (bool T)
bool T is non empty set
bool (bool T) is non empty set
[#] (bool T) is non empty non proper Element of bool (bool T)
bool (bool T) is non empty set
TopStruct(# T,([#] (bool T)) #) is strict TopStruct
T is set
(T) is TopStruct
bool T is non empty Element of bool (bool T)
bool T is non empty set
bool (bool T) is non empty set
[#] (bool T) is non empty non proper Element of bool (bool T)
bool (bool T) is non empty set
TopStruct(# T,([#] (bool T)) #) is strict TopStruct
the carrier of (T) is set
bool the carrier of (T) is non empty set
bool (bool the carrier of (T)) is non empty set
the topology of (T) is Element of bool (bool the carrier of (T))
Z is Element of bool (bool the carrier of (T))
union Z is Element of bool the carrier of (T)
Z is Element of bool the carrier of (T)
F is Element of bool the carrier of (T)
Z /\ F is Element of bool the carrier of (T)
T is non empty set
(T) is strict TopSpace-like TopStruct
bool T is non empty Element of bool (bool T)
bool T is non empty set
bool (bool T) is non empty set
[#] (bool T) is non empty non proper Element of bool (bool T)
bool (bool T) is non empty set
TopStruct(# T,([#] (bool T)) #) is non empty strict TopStruct
T is set
{T} is non empty finite set
({T}) is non empty strict TopSpace-like TopStruct
bool {T} is non empty finite V28() Element of bool (bool {T})
bool {T} is non empty finite V28() set
bool (bool {T}) is non empty finite V28() set
[#] (bool {T}) is non empty non proper finite V28() Element of bool (bool {T})
bool (bool {T}) is non empty finite V28() set
TopStruct(# {T},([#] (bool {T})) #) is non empty strict TopStruct
the carrier of ({T}) is non empty set
X is Element of the carrier of ({T})
Z is Element of the carrier of ({T})
bool the carrier of ({T}) is non empty set
{{}} is non empty finite V28() set
({{}}) is non empty strict TopSpace-like T_0 T_1 T_2 TopStruct
bool {{}} is non empty finite V28() Element of bool (bool {{}})
bool {{}} is non empty finite V28() set
bool (bool {{}}) is non empty finite V28() set
[#] (bool {{}}) is non empty non proper finite V28() Element of bool (bool {{}})
bool (bool {{}}) is non empty finite V28() set
TopStruct(# {{}},([#] (bool {{}})) #) is non empty strict TopStruct
T is non empty TopSpace-like T_0 T_1 T_2 TopStruct
the carrier of T is non empty set
bool the carrier of T is non empty set
X is Element of bool the carrier of T
T is finite set
(T) is strict TopSpace-like TopStruct
bool T is non empty finite V28() Element of bool (bool T)
bool T is non empty finite V28() set
bool (bool T) is non empty finite V28() set
[#] (bool T) is non empty non proper finite V28() Element of bool (bool T)
bool (bool T) is non empty finite V28() set
TopStruct(# T,([#] (bool T)) #) is strict TopStruct
{{}} is non empty finite V28() set
({{}}) is non empty finite strict TopSpace-like T_0 T_1 T_2 TopStruct
bool {{}} is non empty finite V28() Element of bool (bool {{}})
bool {{}} is non empty finite V28() set
bool (bool {{}}) is non empty finite V28() set
[#] (bool {{}}) is non empty non proper finite V28() Element of bool (bool {{}})
bool (bool {{}}) is non empty finite V28() set
TopStruct(# {{}},([#] (bool {{}})) #) is non empty strict TopStruct
T is TopSpace-like TopStruct
the carrier of T is set
bool the carrier of T is non empty set
bool (bool the carrier of T) is non empty set
X is Element of bool (bool the carrier of T)
T is TopSpace-like TopStruct
the carrier of T is set
T is TopSpace-like TopStruct
the carrier of T is set
bool the carrier of T is non empty set
X is Element of bool the carrier of T
Z is finite Element of bool the carrier of T
T | Z is strict TopSpace-like SubSpace of T
[#] (T | Z) is non proper open closed Element of bool the carrier of (T | Z)
the carrier of (T | Z) is set
bool the carrier of (T | Z) is non empty set
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
bool the carrier of T is non empty set
the non empty finite (T) Element of bool the carrier of T is non empty finite (T) Element of bool the carrier of T
T is TopStruct
the carrier of T is set
X is Element of the carrier of T
Z is Element of the carrier of T
bool the carrier of T is non empty set
T is T_0 T_1 T_2 TopStruct
X is SubSpace of T
the carrier of X is set
Z is Element of the carrier of X
F is Element of the carrier of X
bool the carrier of X is non empty set
[#] X is non proper Element of bool the carrier of X
[#] T is non proper Element of bool the carrier of T
the carrier of T is set
bool the carrier of T is non empty set
FF is Element of the carrier of T
G is Element of the carrier of T
c7 is Element of bool the carrier of T
g is Element of bool the carrier of T
c7 /\ ([#] X) is Element of bool the carrier of X
g /\ ([#] X) is Element of bool the carrier of X
the topology of T is Element of bool (bool the carrier of T)
bool (bool the carrier of T) is non empty set
h is Element of bool the carrier of X
the topology of X is Element of bool (bool the carrier of X)
bool (bool the carrier of X) is non empty set
h is Element of bool the carrier of X
c7 /\ g is Element of bool the carrier of T
h /\ h is Element of bool the carrier of X
c7 /\ (g /\ ([#] X)) is Element of bool the carrier of X
(c7 /\ (g /\ ([#] X))) /\ ([#] X) is Element of bool the carrier of X
{} /\ ([#] X) is finite Element of bool the carrier of X
T is TopStruct
the carrier of T is set
bool the carrier of T is non empty set
X is SubSpace of T
the carrier of X is set
bool the carrier of X is non empty set
Z is Element of bool the carrier of T
F is Element of bool the carrier of X
[#] X is non proper Element of bool the carrier of X
FF is Element of bool the carrier of X
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
[#] T is non empty non proper open closed Element of bool the carrier of T
bool the carrier of T is non empty set
X is non empty TopSpace-like TopStruct
the carrier of X is non empty set
[: the carrier of T, the carrier of X:] is non empty set
bool [: the carrier of T, the carrier of X:] is non empty set
Z is Element of the carrier of T
{Z} is non empty finite (T) Element of bool the carrier of T
F is TopSpace-like SubSpace of T
the carrier of F is set
[: the carrier of F, the carrier of X:] is set
bool [: the carrier of F, the carrier of X:] is non empty set
FF is TopSpace-like SubSpace of T
the carrier of FF is set
[: the carrier of FF, the carrier of X:] is set
bool [: the carrier of FF, the carrier of X:] is non empty set
[#] F is non proper open closed Element of bool the carrier of F
bool the carrier of F is non empty set
[#] FF is non proper open closed Element of bool the carrier of FF
bool the carrier of FF is non empty set
([#] F) \/ ([#] FF) is set
([#] F) /\ ([#] FF) is Element of bool the carrier of FF
G is Relation-like the carrier of F -defined the carrier of X -valued Function-like V21( the carrier of F, the carrier of X) Element of bool [: the carrier of F, the carrier of X:]
G . Z is set
c7 is Relation-like the carrier of FF -defined the carrier of X -valued Function-like V21( the carrier of FF, the carrier of X) Element of bool [: the carrier of FF, the carrier of X:]
c7 . Z is set
G +* c7 is Relation-like Function-like set
dom c7 is Element of bool the carrier of FF
rng (G +* c7) is set
rng G is Element of bool the carrier of X
bool the carrier of X is non empty set
rng c7 is Element of bool the carrier of X
(rng G) \/ (rng c7) is Element of bool the carrier of X
dom G is Element of bool the carrier of F
dom (G +* c7) is set
h is Relation-like the carrier of T -defined the carrier of X -valued Function-like V21( the carrier of T, the carrier of X) Element of bool [: the carrier of T, the carrier of X:]
h is Element of bool the carrier of X
h " h is Element of bool the carrier of T
G " h is Element of bool the carrier of F
c7 " h is Element of bool the carrier of FF
dom h is Element of bool the carrier of T
(dom G) \/ (dom c7) is set
P2 is set
(h " h) /\ ([#] FF) is Element of bool the carrier of FF
h . P2 is set
c7 . P2 is set
c7 . P2 is set
h . P2 is set
P2 is set
h . P2 is set
G . P2 is set
P2 is set
(h " h) /\ ([#] F) is Element of bool the carrier of F
h . P2 is set
G . P2 is set
G . P2 is set
h . P2 is set
P is Element of bool the carrier of T
P1 is Element of bool the carrier of T
(h " h) /\ (([#] F) \/ ([#] FF)) is Element of bool the carrier of T
((h " h) /\ ([#] F)) \/ ((h " h) /\ ([#] FF)) is set
(G " h) \/ (c7 " h) is set
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
X is non empty TopSpace-like TopStruct
the carrier of X is non empty set
[#] X is non empty non proper open closed Element of bool the carrier of X
bool the carrier of X is non empty set
[: the carrier of X, the carrier of T:] is non empty set
bool [: the carrier of X, the carrier of T:] is non empty set
Z is TopSpace-like SubSpace of X
the carrier of Z is set
[: the carrier of Z, the carrier of T:] is set
bool [: the carrier of Z, the carrier of T:] is non empty set
F is TopSpace-like SubSpace of X
the carrier of F is set
[: the carrier of F, the carrier of T:] is set
bool [: the carrier of F, the carrier of T:] is non empty set
[#] Z is non proper open closed Element of bool the carrier of Z
bool the carrier of Z is non empty set
[#] F is non proper open closed Element of bool the carrier of F
bool the carrier of F is non empty set
([#] Z) \/ ([#] F) is set
([#] Z) /\ ([#] F) is Element of bool the carrier of F
FF is Element of the carrier of X
G is Element of the carrier of X
{FF,G} is non empty finite (X) Element of bool the carrier of X
c7 is Relation-like the carrier of Z -defined the carrier of T -valued Function-like V21( the carrier of Z, the carrier of T) Element of bool [: the carrier of Z, the carrier of T:]
c7 . FF is set
c7 . G is set
g is Relation-like the carrier of F -defined the carrier of T -valued Function-like V21( the carrier of F, the carrier of T) Element of bool [: the carrier of F, the carrier of T:]
g . FF is set
g . G is set
c7 +* g is Relation-like Function-like set
dom g is Element of bool the carrier of F
rng (c7 +* g) is set
rng c7 is Element of bool the carrier of T
bool the carrier of T is non empty set
rng g is Element of bool the carrier of T
(rng c7) \/ (rng g) is Element of bool the carrier of T
dom c7 is Element of bool the carrier of Z
dom (c7 +* g) is set
h is Relation-like the carrier of X -defined the carrier of T -valued Function-like V21( the carrier of X, the carrier of T) Element of bool [: the carrier of X, the carrier of T:]
P is Element of bool the carrier of T
h " P is Element of bool the carrier of X
c7 " P is Element of bool the carrier of Z
g " P is Element of bool the carrier of F
dom h is Element of bool the carrier of X
(dom c7) \/ (dom g) is set
x is set
(h " P) /\ ([#] F) is Element of bool the carrier of F
h . x is set
g . x is set
g . x is set
h . x is set
x is set
h . x is set
c7 . x is set
x is set
(h " P) /\ ([#] Z) is Element of bool the carrier of Z
h . x is set
c7 . x is set
c7 . x is set
h . x is set
P1 is Element of bool the carrier of X
P2 is Element of bool the carrier of X
(h " P) /\ (([#] Z) \/ ([#] F)) is Element of bool the carrier of X
((h " P) /\ ([#] Z)) \/ ((h " P) /\ ([#] F)) is set
(c7 " P) \/ (g " P) is set
T is TopStruct
the topology of T is Element of bool (bool the carrier of T)
the carrier of T is set
bool the carrier of T is non empty set
bool (bool the carrier of T) is non empty set
X is Element of bool the carrier of T
T is TopSpace-like TopStruct
the carrier of T is set
bool the carrier of T is non empty set
bool (bool the carrier of T) is non empty set
the topology of T is non empty open Element of bool (bool the carrier of T)
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
bool the carrier of T is non empty set
bool (bool the carrier of T) is non empty set
the topology of T is non empty open Element of bool (bool the carrier of T)
TopStruct(# the carrier of T, the topology of T #) is non empty strict TopSpace-like TopStruct
the carrier of TopStruct(# the carrier of T, the topology of T #) is non empty set
bool the carrier of TopStruct(# the carrier of T, the topology of T #) is non empty set
bool (bool the carrier of TopStruct(# the carrier of T, the topology of T #)) is non empty set
X is set
Z is Element of bool (bool the carrier of TopStruct(# the carrier of T, the topology of T #))
F is Element of bool the carrier of TopStruct(# the carrier of T, the topology of T #)
Z is Element of bool (bool the carrier of T)
F is Element of bool the carrier of T
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
bool the carrier of T is non empty set
the topology of T is non empty open Element of bool (bool the carrier of T)
bool (bool the carrier of T) is non empty set
TopStruct(# the carrier of T, the topology of T #) is non empty strict TopSpace-like TopStruct
the carrier of TopStruct(# the carrier of T, the topology of T #) is non empty set
bool the carrier of TopStruct(# the carrier of T, the topology of T #) is non empty set
X is set
Z is Element of bool the carrier of TopStruct(# the carrier of T, the topology of T #)
bool (bool the carrier of TopStruct(# the carrier of T, the topology of T #)) is non empty set
F is Element of bool (bool the carrier of TopStruct(# the carrier of T, the topology of T #))
FF is Element of bool (bool the carrier of T)
G is Element of bool (bool the carrier of TopStruct(# the carrier of T, the topology of T #))
Z is Element of bool the carrier of T
F is Element of bool (bool the carrier of T)
bool (bool the carrier of TopStruct(# the carrier of T, the topology of T #)) is non empty set
FF is Element of bool (bool the carrier of TopStruct(# the carrier of T, the topology of T #))
G is Element of bool (bool the carrier of T)