K166() is Element of bool K162()
K162() is set
bool K162() is non empty cup-closed diff-closed preBoolean set
omega is set
bool omega is non empty cup-closed diff-closed preBoolean set
bool K166() is non empty cup-closed diff-closed preBoolean set
{} is empty finite V40() set
the empty finite V40() set is empty finite V40() set
1 is non empty set
union {} is finite set
meet {} is set
{{}} is non empty finite V40() set
x is set
T is set
Fin T is non empty cup-closed diff-closed preBoolean set
X is set
T is set
bool T is non empty cup-closed diff-closed preBoolean set
bool (bool T) is non empty cup-closed diff-closed preBoolean set
Fin T is non empty cup-closed diff-closed preBoolean set
x is Element of bool (bool T)
meet x is Element of bool T
X is set
T is set
bool T is non empty cup-closed diff-closed preBoolean set
bool (bool T) is non empty cup-closed diff-closed preBoolean set
x is Element of bool (bool T)
COMPLEMENT x is Element of bool (bool T)
X is Relation-like Function-like set
dom X is set
rng X is set
Y is set
Q is set
X . Y is set
X . Q is set
c6 is Element of bool T
c6 ` is Element of bool T
T \ c6 is set
S29 is Element of bool T
S29 ` is Element of bool T
T \ S29 is set
(S29 `) ` is Element of bool T
T \ (S29 `) is set
Y is set
Q is set
X . Q is set
c6 is Element of bool T
c6 ` is Element of bool T
T \ c6 is set
Y is set
Q is Element of bool T
Q ` is Element of bool T
T \ Q is set
(Q `) ` is Element of bool T
T \ (Q `) is set
X . (Q `) is set
T is set
x is set
card T is cardinal set
card x is cardinal set
T is 1-sorted
the carrier of T is set
bool the carrier of T is non empty cup-closed diff-closed preBoolean set
bool (bool the carrier of T) is non empty cup-closed diff-closed preBoolean set
x is Element of bool (bool the carrier of T)
COMPLEMENT x is Element of bool (bool the carrier of T)
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
(X `) ` is Element of bool the carrier of T
the carrier of T \ (X `) is set
T is 1-sorted
the carrier of T is set
bool the carrier of T is non empty cup-closed diff-closed preBoolean set
bool (bool the carrier of T) is non empty cup-closed diff-closed preBoolean set
x is Element of bool (bool the carrier of T)
COMPLEMENT x is Element of bool (bool the carrier of T)
Intersect (COMPLEMENT x) 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
meet (COMPLEMENT x) is Element of bool the carrier of T
[#] the carrier of T is non proper Element of bool the carrier of T
([#] the carrier of T) \ (union x) is Element of bool the carrier of T
X is empty proper finite V40() Element of bool (bool the carrier of T)
COMPLEMENT X is empty proper finite V40() Element of bool (bool the carrier of T)
T is 1-sorted
the carrier of T is set
bool the carrier of T is non empty cup-closed diff-closed preBoolean set
bool (bool the carrier of T) is non empty cup-closed diff-closed preBoolean set
x is Element of bool (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
Intersect x is Element of bool the carrier of T
(Intersect x) ` is Element of bool the carrier of T
the carrier of T \ (Intersect x) is set
(union (COMPLEMENT x)) ` is Element of bool the carrier of T
the carrier of T \ (union (COMPLEMENT x)) is set
((union (COMPLEMENT x)) `) ` is Element of bool the carrier of T
the carrier of T \ ((union (COMPLEMENT x)) `) is set
COMPLEMENT (COMPLEMENT x) is Element of bool (bool the carrier of T)
Intersect (COMPLEMENT (COMPLEMENT x)) is Element of bool the carrier of T
(Intersect (COMPLEMENT (COMPLEMENT x))) ` is Element of bool the carrier of T
the carrier of T \ (Intersect (COMPLEMENT (COMPLEMENT x))) 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 cup-closed diff-closed preBoolean set
X is Element of bool the carrier of T
x is Element of bool the carrier of T
Cl X is 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 cup-closed diff-closed preBoolean set
bool (bool the carrier of T) is non empty cup-closed diff-closed preBoolean set
x is quasi_basis open Element of bool (bool the carrier of T)
X is Element of bool the carrier of T
{ b1 where b1 is Element of bool the carrier of T : ( b1 in x & b1 c= X ) } is set
union { b1 where b1 is Element of bool the carrier of T : ( b1 in x & b1 c= X ) } is set
the topology of T is Element of bool (bool the carrier of T)
UniCl x is Element of bool (bool the carrier of T)
Q is set
c6 is Element of bool (bool the carrier of T)
union c6 is Element of bool the carrier of T
S29 is set
b is set
a9 is Element of bool the carrier of T
c6 is set
S29 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 cup-closed diff-closed preBoolean set
bool (bool the carrier of T) is non empty cup-closed diff-closed preBoolean set
x is quasi_basis open Element of bool (bool the carrier of T)
X is Element of bool the carrier of T
the topology of T is 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 cup-closed diff-closed preBoolean set
bool (bool the carrier of T) is non empty cup-closed diff-closed preBoolean set
x is quasi_basis open Element of bool (bool the carrier of T)
X is Element of bool the carrier of T
Int X is open Element of bool the carrier of T
{ b1 where b1 is Element of bool the carrier of T : ( b1 in x & b1 c= X ) } is set
union { b1 where b1 is Element of bool the carrier of T : ( b1 in x & b1 c= X ) } is set
{ b1 where b1 is Element of bool the carrier of T : ( b1 in x & b1 c= Int X ) } is set
c6 is set
S29 is Element of bool the carrier of T
c6 is set
S29 is Element of bool the carrier of T
T is non empty TopStruct
the carrier of T is non empty set
bool the carrier of T is non empty cup-closed diff-closed preBoolean set
bool (bool the carrier of T) is non empty cup-closed diff-closed preBoolean set
T is non empty TopStruct
the carrier of T is non empty set
bool the carrier of T is non empty cup-closed diff-closed preBoolean set
bool (bool the carrier of T) is non empty cup-closed diff-closed preBoolean set
x is Element of the carrier of T
the topology of T is Element of bool (bool the carrier of T)
{ b1 where b1 is Element of bool the carrier of T : S1[b1] } is set
Y is Element of bool (bool the carrier of T)
Q is set
c6 is Element of bool the carrier of T
Q is set
c6 is Element of bool the carrier of T
Intersect Y is Element of bool the carrier of T
Q is Element of bool the carrier of T
c6 is Element of bool the carrier of T
T is non empty TopStruct
the carrier of T is non empty set
T is non empty TopStruct
the carrier of T is non empty set
bool the carrier of T is non empty cup-closed diff-closed preBoolean set
bool (bool the carrier of T) is non empty cup-closed diff-closed preBoolean set
x is Element of the carrier of T
X is open (T,x) Element of bool (bool the carrier of T)
Y is Element of bool the carrier of T
the topology of T is Element of bool (bool the carrier of T)
Intersect X is Element of bool the carrier of T
T is non empty TopStruct
the carrier of T is non empty set
x is Element of the carrier of T
bool the carrier of T is non empty cup-closed diff-closed preBoolean set
bool (bool the carrier of T) is non empty cup-closed diff-closed preBoolean set
Y is Element of bool the carrier of T
X is open (T,x) Element of bool (bool the carrier of T)
T is non empty TopStruct
the carrier of T is non empty set
bool the carrier of T is non empty cup-closed diff-closed preBoolean set
bool (bool the carrier of T) is non empty cup-closed diff-closed preBoolean set
the topology of T is Element of bool (bool the carrier of T)
x is Element of bool (bool the carrier of T)
X is set
UniCl x is Element of bool (bool the carrier of T)
Y is Element of bool the carrier of T
{ b1 where b1 is Element of bool the carrier of T : ( b1 in x & b1 c= Y ) } is set
c6 is set
S29 is Element of bool the carrier of T
c6 is Element of bool (bool the carrier of T)
S29 is set
b is Element of the carrier of T
a9 is open (T,b) Element of bool (bool the carrier of T)
b9 is Element of bool the carrier of T
Z is set
Z is set
b is set
a9 is Element of bool the carrier of T
union c6 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 cup-closed diff-closed preBoolean set
bool (bool the carrier of T) is non empty cup-closed diff-closed preBoolean set
x is Element of bool (bool the carrier of T)
COMPLEMENT x is Element of bool (bool the carrier of T)
X is Element of bool (bool the carrier of T)
Y is Element of bool the carrier of T
Y ` is Element of bool the carrier of T
the carrier of T \ Y is set
Intersect X 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
Y is Element of bool the carrier of T
x is Element of bool (bool the carrier of T)
Intersect x is Element of bool the carrier of T
X is Element of bool the carrier of T
COMPLEMENT x is Element of bool (bool the carrier of T)
Y is Element of bool (bool the carrier of T)
Q is Element of bool the carrier of T
Q ` is Element of bool the carrier of T
the carrier of T \ Q is set
union Y is Element of bool the carrier of T
(Intersect x) ` is Element of bool the carrier of T
the carrier of T \ (Intersect x) is set
T is TopStruct
the carrier of T is set
bool the carrier of T is non empty cup-closed diff-closed preBoolean set
T is TopStruct
the carrier of T is set
bool the carrier of T is non empty cup-closed diff-closed preBoolean set
x 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 cup-closed diff-closed preBoolean set
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
bool the carrier of T is non empty cup-closed diff-closed preBoolean set
x is Element of bool the carrier of T
X is Element of the carrier of T
{X} is non empty finite Element of bool the carrier of T
Cl {X} is closed Element of bool the carrier of T
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
x is Element of the carrier of T
{x} is non empty finite Element of bool the carrier of T
bool the carrier of T is non empty cup-closed diff-closed preBoolean set
Cl {x} is closed Element of bool the carrier of T
X is Element of bool the carrier of T
Y is Element of bool the carrier of T
X \/ Y 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 cup-closed diff-closed preBoolean set
the Element of the carrier of T is Element of the carrier of T
{ the Element of the carrier of T} is non empty finite Element of bool the carrier of T
Cl { the Element of the carrier of T} is closed Element of bool the carrier of T
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
x is Element of the carrier of T
{x} is non empty finite Element of bool the carrier of T
bool the carrier of T is non empty cup-closed diff-closed preBoolean set
Cl {x} is closed Element of bool the carrier of T
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
x is Element of the carrier of T
{x} is non empty finite Element of bool the carrier of T
bool the carrier of T is non empty cup-closed diff-closed preBoolean set
Cl {x} is closed 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 cup-closed diff-closed preBoolean set
x is Element of bool the carrier of T
X is Element of bool the carrier of T
X \ 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
X /\ (x `) is Element of bool the carrier of T
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 cup-closed diff-closed preBoolean set
x is non empty (T) Element of bool the carrier of T
X is Element of the carrier of T
Y is Element of the carrier of T
Q is Element of bool the carrier of T
c6 is Element of bool the carrier of T
x \ Q is Element of bool the carrier of T
x \ c6 is Element of bool the carrier of T
Q /\ c6 is Element of bool the carrier of T
(x \ Q) \/ (x \ c6) is Element of bool the carrier of T
x \ (Q /\ c6) is Element of bool the carrier of T
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 cup-closed diff-closed preBoolean set
x is Element of bool the carrier of T
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 cup-closed diff-closed preBoolean set
x is non empty trivial finite (T) Element of bool the carrier of T
X is Element of x
{X} is non empty trivial finite Element of bool x
bool x is non empty cup-closed diff-closed preBoolean finite V40() set
Y is Element of the carrier of T
Q is Element of the carrier of T
T is non empty TopSpace-like TopStruct
the non empty TopSpace-like T_0 T_1 T_2 () TopStruct is non empty TopSpace-like T_0 T_1 T_2 () TopStruct
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
x is Element of the carrier of T
{x} is non empty finite Element of bool the carrier of T
bool the carrier of T is non empty cup-closed diff-closed preBoolean set
Cl {x} is closed Element of bool the carrier of T
X is Element of the carrier of T
{X} is non empty finite Element of bool the carrier of T
Cl {X} is closed Element of bool the carrier of T
x is Element of the carrier of T
X is Element of the carrier of T
{x} is non empty finite Element of bool the carrier of T
bool the carrier of T is non empty cup-closed diff-closed preBoolean set
Cl {x} is closed Element of bool the carrier of T
{X} is non empty finite Element of bool the carrier of T
Cl {X} is closed Element of bool the carrier of T
T is non empty TopSpace-like () TopStruct
the carrier of T is non empty set
x is Element of the carrier of T
{x} is non empty finite Element of bool the carrier of T
bool the carrier of T is non empty cup-closed diff-closed preBoolean set
Cl {x} is closed Element of bool the carrier of T
X is Element of the carrier of T
{X} is non empty finite Element of bool the carrier of T
Cl {X} is closed Element of bool the carrier of T
Y is Element of the carrier of T
T is non empty TopSpace-like TopStruct
T is set
{T} is non empty finite set
Fin T is non empty cup-closed diff-closed preBoolean set
{T} \/ (Fin T) is non empty set
bool T is non empty cup-closed diff-closed preBoolean Element of bool (bool T)
bool T is non empty cup-closed diff-closed preBoolean set
bool (bool T) is non empty cup-closed diff-closed preBoolean set
x is Element of bool (bool T)
X is Element of bool (bool T)
COMPLEMENT X is Element of bool (bool T)
TopStruct(# T,(COMPLEMENT X) #) is strict TopStruct
Y is strict TopStruct
the carrier of Y is set
the topology of Y is Element of bool (bool the carrier of Y)
bool the carrier of Y is non empty cup-closed diff-closed preBoolean set
bool (bool the carrier of Y) is non empty cup-closed diff-closed preBoolean set
COMPLEMENT the topology of Y is Element of bool (bool the carrier of Y)
x is strict TopStruct
the carrier of x is set
the topology of x is Element of bool (bool the carrier of x)
bool the carrier of x is non empty cup-closed diff-closed preBoolean set
bool (bool the carrier of x) is non empty cup-closed diff-closed preBoolean set
COMPLEMENT the topology of x is Element of bool (bool the carrier of x)
X is strict TopStruct
the carrier of X is set
the topology of X is Element of bool (bool the carrier of X)
bool the carrier of X is non empty cup-closed diff-closed preBoolean set
bool (bool the carrier of X) is non empty cup-closed diff-closed preBoolean set
COMPLEMENT the topology of X is Element of bool (bool the carrier of X)
T is non empty set
(T) is strict TopStruct
T is set
(T) is strict TopStruct
bool T is non empty cup-closed diff-closed preBoolean set
bool (bool T) is non empty cup-closed diff-closed preBoolean set
Fin T is non empty cup-closed diff-closed preBoolean set
{T} is non empty finite set
X is Element of bool (bool T)
x is Element of bool (bool T)
the carrier of (T) is set
the topology of (T) is Element of bool (bool the carrier of (T))
bool the carrier of (T) is non empty cup-closed diff-closed preBoolean set
bool (bool the carrier of (T)) is non empty cup-closed diff-closed preBoolean set
COMPLEMENT the topology of (T) is Element of bool (bool the carrier of (T))
{T} \/ (Fin T) is non empty set
COMPLEMENT (COMPLEMENT the topology of (T)) is Element of bool (bool the carrier of (T))
Q is Element of bool (bool T)
COMPLEMENT Q is Element of bool (bool T)
c6 is Element of bool (bool T)
COMPLEMENT c6 is Element of bool (bool T)
(COMPLEMENT Q) \/ (COMPLEMENT c6) is Element of bool (bool T)
{{}} \/ (COMPLEMENT c6) is non empty set
{}. T is empty finite V40() Element of Fin T
{} T is empty finite V40() Element of bool T
({} T) ` is Element of bool T
T \ ({} T) is set
(({} T) `) ` is Element of bool T
T \ (({} T) `) is set
[#] T is non proper Element of bool T
S29 is Element of bool (bool the carrier of (T))
union S29 is Element of bool the carrier of (T)
S29 /\ (COMPLEMENT c6) is Element of bool (bool T)
a9 is Element of bool (bool T)
S29 /\ {{}} is finite Element of bool (bool the carrier of (T))
union (S29 /\ {{}}) is Element of bool the carrier of (T)
S29 /\ the topology of (T) is Element of bool (bool the carrier of (T))
union (S29 /\ the topology of (T)) is Element of bool the carrier of (T)
(S29 /\ {{}}) \/ (S29 /\ (COMPLEMENT c6)) is set
union ((S29 /\ {{}}) \/ (S29 /\ (COMPLEMENT c6))) is set
union (S29 /\ (COMPLEMENT c6)) is Element of bool T
(union (S29 /\ {{}})) \/ (union (S29 /\ (COMPLEMENT c6))) is set
b9 is Element of bool (bool T)
union b9 is Element of bool T
COMPLEMENT b9 is Element of bool (bool T)
meet (COMPLEMENT b9) is Element of bool T
([#] T) \ (union b9) is Element of bool T
(union b9) ` is Element of bool T
T \ (union b9) is set
S29 is Element of bool the carrier of (T)
b is Element of bool the carrier of (T)
S29 /\ b is Element of bool the carrier of (T)
S29 /\ b is Element of bool the carrier of (T)
b9 is Element of bool T
b9 ` is Element of bool T
T \ b9 is set
a9 is Element of bool T
a9 ` is Element of bool T
T \ a9 is set
(a9 `) \/ (b9 `) is Element of bool T
a9 /\ b9 is Element of bool T
(a9 /\ b9) ` is Element of bool T
T \ (a9 /\ b9) is set
S29 /\ b is Element of bool the carrier of (T)
T is non empty set
(T) is non empty strict TopSpace-like TopStruct
the carrier of (T) is non empty set
bool the carrier of (T) is non empty cup-closed diff-closed preBoolean 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 topology of (T) is non empty Element of bool (bool the carrier of (T))
bool (bool the carrier of (T)) is non empty cup-closed diff-closed preBoolean set
COMPLEMENT the topology of (T) is Element of bool (bool the carrier of (T))
{T} is non empty with_non-empty_elements non empty-membered finite set
Fin T is non empty cup-closed diff-closed preBoolean set
{T} \/ (Fin T) is non empty set
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
x is Element of the carrier of T
{x} is non empty finite Element of bool the carrier of T
bool the carrier of T is non empty cup-closed diff-closed preBoolean set
Cl {x} is closed Element of bool the carrier of T
T is non empty set
(T) is non empty strict TopSpace-like TopStruct
the carrier of (T) is non empty set
x is Element of the carrier of (T)
{x} is non empty finite Element of bool the carrier of (T)
bool the carrier of (T) is non empty cup-closed diff-closed preBoolean set
T is non empty non trivial non empty-membered non finite set
(T) is non empty strict TopSpace-like T_0 T_1 TopStruct
the carrier of (T) is non empty set
bool the carrier of (T) is non empty cup-closed diff-closed preBoolean set
[#] T is non empty non proper Element of bool T
bool T is non empty cup-closed diff-closed preBoolean set
X is Element of bool the carrier of (T)
[#] (T) is non empty non proper open closed dense non boundary Element of bool the carrier of (T)
Y is Element of bool the carrier of (T)
Q is Element of bool the carrier of (T)
Y \/ Q is Element of bool the carrier of (T)
c6 is finite set
S29 is finite set
c6 \/ S29 is finite set
Y is non empty ((T)) Element of bool the carrier of (T)
Q is Element of the carrier of (T)
{Q} is non empty finite Element of bool the carrier of (T)
Cl {Q} is closed Element of bool the carrier of (T)
the non empty non trivial non empty-membered non finite set is non empty non trivial non empty-membered non finite set
( the non empty non trivial non empty-membered non finite set ) is non empty strict TopSpace-like T_0 T_1 () TopStruct
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
bool the carrier of T is non empty cup-closed diff-closed preBoolean set
x is Element of the carrier of T
X is Element of bool the carrier of T
Int X is open Element of bool the carrier of T
(Int X) ` is closed Element of bool the carrier of T
the carrier of T \ (Int X) is set
((Int X) `) ` is open Element of bool the carrier of T
the carrier of T \ ((Int X) `) is set
[#] T is non empty non proper open closed dense non boundary Element of bool the carrier of T
Y is non empty non proper open closed dense non boundary Element of bool the carrier of T
Int Y is open Element of bool the carrier of T
[#] T is non empty non proper open closed dense non boundary Element of bool the carrier of T
Y is Element of bool the carrier of T
Q is Element of bool the carrier of T
Q ` is Element of bool the carrier of T
the carrier of T \ Q is set
c6 is Element of bool the carrier of T
c6 ` is Element of bool the carrier of T
the carrier of T \ c6 is set
Int c6 is open Element of bool the carrier of T
[#] T is non empty non proper open closed dense non boundary Element of bool the carrier of T
x is Element of the carrier of T
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
Int (X `) is open Element of bool the carrier of T
Y is Element of bool the carrier of T
Int Y is open Element of bool the carrier of T
Q is Element of bool the carrier of T
Y ` is Element of bool the carrier of T
the carrier of T \ Y is set
c6 is Element of bool the carrier of T
(X `) ` is Element of bool the carrier of T
the carrier of T \ (X `) 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 cup-closed diff-closed preBoolean set
x is Element of the carrier of T
[#] T is non empty non proper open closed dense non boundary Element of bool the carrier of T
X is Element of bool the carrier of T
Int X is open Element of bool the carrier of T
x is Element of the carrier of T
X is Element of bool the carrier of T
Int X is open Element of bool the carrier of T
Y is Element of bool the carrier of T
Int Y is open Element of bool the carrier of T
(Int X) /\ (Int Y) is open Element of bool the carrier of T
X /\ Y is Element of bool the carrier of T
Int (X /\ Y) is open Element of bool the carrier of T
Q is Element of bool the carrier of T
Int Q is open Element of bool the carrier of T