:: YELLOW_8 semantic presentation

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

c

c

T \ c

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

c

c

T \ c

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

{ b

union { b

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

c

union c

S29 is set

b is set

a9 is Element of bool the carrier of T

c

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

{ b

union { b

{ b

c

S29 is Element of bool the carrier of T

c

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)

{ b

Y is Element of bool (bool the carrier of T)

Q is set

c

Q is set

c

Intersect Y is Element of bool the carrier of T

Q is Element of bool the carrier of T

c

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

{ b

c

S29 is Element of bool the carrier of T

c

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 c

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

c

x \ Q is Element of bool the carrier of T

x \ c

Q /\ c

(x \ Q) \/ (x \ c

x \ (Q /\ c

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)

c

COMPLEMENT c

(COMPLEMENT Q) \/ (COMPLEMENT c

{{}} \/ (COMPLEMENT c

{}. 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 c

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 c

union ((S29 /\ {{}}) \/ (S29 /\ (COMPLEMENT c

union (S29 /\ (COMPLEMENT c

(union (S29 /\ {{}})) \/ (union (S29 /\ (COMPLEMENT c

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)

c

S29 is finite set

c

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

c

c

the carrier of T \ c

Int c

[#] 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

c

(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