:: YELLOW_8 semantic presentation

K166() is Element of bool K162()
K162() is set

omega is set

the empty finite V40() set is empty finite V40() set
1 is non empty set

is non empty finite V40() set
x is set
T is set

X is set
T is set

bool (bool 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 (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)

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

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 () is Element of bool the carrier of T
union x is Element of bool the carrier of T
() ` is Element of bool the carrier of T
the carrier of T \ () is set
meet () 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) \ () 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 () is Element of bool the carrier of T
Intersect x is Element of bool the carrier of T
() ` is Element of bool the carrier of T
the carrier of T \ () is set
(union ()) ` is Element of bool the carrier of T
the carrier of T \ (union ()) is set
((union ()) `) ` is Element of bool the carrier of T
the carrier of T \ ((union ()) `) is set
COMPLEMENT () is Element of bool (bool the carrier of T)
Intersect () is Element of bool the carrier of T
() ` is Element of bool the carrier of T
the carrier of T \ () 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
() ` is Element of bool the carrier of T
the carrier of T \ () 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
() ` is Element of bool the carrier of T
the carrier of T \ () 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

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

{T} \/ (Fin T) is non empty set
bool T is non empty cup-closed diff-closed preBoolean Element of bool (bool T)

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,() #) 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)

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)

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 (bool 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)
() \/ () is Element of bool (bool T)
\/ () 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 /\ () 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 /\ ()) is set
union ((S29 /\ ) \/ (S29 /\ ())) is set
union (S29 /\ ()) is Element of bool T
(union (S29 /\ )) \/ (union (S29 /\ ())) 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 () 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} \/ (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

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