:: TOPGEN_4 semantic presentation

REAL is non empty non trivial non finite set

NAT is non trivial ordinal non finite cardinal limit_cardinal countable denumerable Element of bool REAL

bool REAL is non empty non trivial non finite set

ExtREAL is non empty set

[:NAT,ExtREAL:] is non trivial non finite set

bool [:NAT,ExtREAL:] is non empty non trivial non finite set

bool ExtREAL is non empty set

omega is non trivial ordinal non finite cardinal limit_cardinal countable denumerable set

bool omega is non empty non trivial non finite set

[:NAT,REAL:] is non trivial non finite set

bool [:NAT,REAL:] is non empty non trivial non finite set

bool (bool REAL) is non empty non trivial non finite set

K302() is V165() TopStruct

the carrier of K302() is V58() set

1 is non empty finite countable Element of NAT

[:1,1:] is non empty finite countable set

bool [:1,1:] is non empty finite V40() countable set

[:[:1,1:],1:] is non empty finite countable set

bool [:[:1,1:],1:] is non empty finite V40() countable set

[:[:1,1:],REAL:] is non empty non trivial non finite set

bool [:[:1,1:],REAL:] is non empty non trivial non finite set

[:REAL,REAL:] is non empty non trivial non finite set

[:[:REAL,REAL:],REAL:] is non empty non trivial non finite set

bool [:[:REAL,REAL:],REAL:] is non empty non trivial non finite set

2 is non empty finite countable Element of NAT

[:2,2:] is non empty finite countable set

[:[:2,2:],REAL:] is non empty non trivial non finite set

bool [:[:2,2:],REAL:] is non empty non trivial non finite set

K330() is V151() V165() L7()

R^1 is non empty strict TopSpace-like T_0 T_1 T_2 V165() TopStruct

{} is set

the empty ordinal natural finite V40() cardinal {} -element countable set is empty ordinal natural finite V40() cardinal {} -element countable set

meet {} is set

union {} is set

the carrier of R^1 is non empty V58() set

RAT is non empty non trivial non finite set

card RAT is non empty non trivial ordinal non finite cardinal set

K466() is non trivial ordinal non finite cardinal set

card REAL is non empty non trivial ordinal non finite cardinal set

T is 1-sorted

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

T is set

bool T is non empty set

bool (bool T) is non empty set

A is Element of bool (bool T)

COMPLEMENT A is Element of bool (bool T)

T is set

card T is ordinal cardinal set

card T is ordinal cardinal set

A is Relation-like Function-like set

proj1 A is set

proj2 A is set

{ {b

T is Relation-like Function-like set

proj1 T is set

proj2 T is set

A is set

F is Element of RAT

{F} is non empty trivial finite 1 -element countable Element of bool RAT

bool RAT is non empty non trivial non finite set

T . F 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

A is Element of bool the carrier of T

Der A is Element of bool the carrier of T

{ b

F is set

{F} is non empty trivial finite 1 -element countable set

A \ {F} is Element of bool the carrier of T

Cl (A \ {F}) is closed Element of bool the carrier of T

F is set

Z is Element of the carrier of T

{Z} is non empty trivial finite 1 -element countable V127(T) Element of bool the carrier of T

A \ {Z} is Element of bool the carrier of T

Cl (A \ {Z}) is closed Element of bool the carrier of T

T is TopStruct

A is finite V259() countable TopStruct

weight A is ordinal cardinal set

T is set

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 set

A is Element of bool the carrier of T

Der A is Element of bool the carrier of T

Cl A is closed Element of bool the carrier of T

A \/ (Der A) 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 set

bool (bool the carrier of T) is non empty set

A is open V253(T) Element of bool (bool the carrier of T)

F is Element of bool the carrier of T

Z is set

{ b

union { b

Z9 is set

Y is Element of bool the carrier of T

T is non empty TopSpace-like TopStruct

density T is ordinal cardinal set

weight T is ordinal cardinal set

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 open V253(T) Element of bool (bool the carrier of T) is open V253(T) Element of bool (bool the carrier of T)

F is open V253(T) Element of bool (bool the carrier of T)

card F is ordinal cardinal set

{ H

Z9 is set

Y is Element of bool the carrier of T

choose Y is Element of Y

the Element of Y is Element of Y

Z9 is Element of bool the carrier of T

Y is Element of bool the carrier of T

Z is Element of bool the carrier of T

choose Z is Element of Z

the Element of Z is Element of Z

card Z9 is ordinal cardinal set

card { H

T is non empty TopSpace-like TopStruct

the carrier of T is non empty set

bool the carrier of T is non empty set

density T is ordinal cardinal set

A is Element of bool the carrier of T

card A is ordinal cardinal set

A is Element of bool the carrier of T

card A is ordinal cardinal set

T is non empty TopSpace-like TopStruct

weight T is ordinal cardinal set

density T is ordinal cardinal set

T is non empty TopSpace-like TopStruct

T is non empty TopSpace-like TopStruct

the carrier of T is non empty set

bool the carrier of T is non empty set

A is Element of bool the carrier of T

F is Element of bool the carrier of T

A \/ F is Element of bool the carrier of T

Fr (A \/ F) is closed Element of bool the carrier of T

Fr A is closed Element of bool the carrier of T

Fr F is closed Element of bool the carrier of T

(Fr A) \/ (Fr F) is closed Element of bool the carrier of T

A /\ F is Element of bool the carrier of T

Fr (A /\ F) is closed Element of bool the carrier of T

(Fr (A \/ F)) \/ (Fr (A /\ F)) is closed Element of bool the carrier of T

(Fr A) /\ (Fr F) is closed Element of bool the carrier of T

((Fr (A \/ F)) \/ (Fr (A /\ F))) \/ ((Fr A) /\ (Fr F)) is closed Element of bool the carrier of T

{} T is empty proper ordinal natural finite V40() cardinal {} -element countable open closed boundary nowhere_dense V124(T) V127(T) dense-in-itself perfect scattered Element of bool the carrier of T

Fr ({} T) is empty proper ordinal natural finite V40() cardinal {} -element countable open closed boundary nowhere_dense V124(T) V127(T) dense-in-itself perfect scattered Element of bool the carrier of T

Cl F is closed Element of bool the carrier of T

Cl A is closed Element of bool the carrier of T

Z is set

F ` is Element of bool the carrier of T

the carrier of T \ F is set

Cl (F `) is closed Element of bool the carrier of T

(Cl F) /\ (Cl (F `)) is closed Element of bool the carrier of T

A ` is Element of bool the carrier of T

the carrier of T \ A is set

Cl (A `) is closed Element of bool the carrier of T

(Cl A) /\ (Cl (A `)) is closed Element of bool the carrier of T

(Cl A) \/ (Cl F) is closed Element of bool the carrier of T

Cl (A \/ F) is closed Element of bool the carrier of T

(A `) /\ (F `) is Element of bool the carrier of T

(A \/ F) ` is Element of bool the carrier of T

the carrier of T \ (A \/ F) is set

Cl ((A \/ F) `) is closed Element of bool the carrier of T

(Cl (A \/ F)) /\ (Cl ((A \/ F) `)) 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 set

bool (bool the carrier of T) is non empty set

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

union A is Element of bool the carrier of T

Fr (union A) is closed Element of bool the carrier of T

Fr A is Element of bool (bool the carrier of T)

union (Fr A) is Element of bool the carrier of T

Cl (union A) is closed Element of bool the carrier of T

clf A is Element of bool (bool the carrier of T)

union (clf A) is Element of bool the carrier of T

F is set

(union A) ` is Element of bool the carrier of T

the carrier of T \ (union A) is set

Cl ((union A) `) is closed Element of bool the carrier of T

(Cl (union A)) /\ (Cl ((union A) `)) is closed Element of bool the carrier of T

Z is set

Z9 is Element of bool the carrier of T

Cl Z9 is closed Element of bool the carrier of T

Z9 ` is Element of bool the carrier of T

the carrier of T \ Z9 is set

Cl (Z9 `) is closed Element of bool the carrier of T

(Cl Z9) /\ (Cl (Z9 `)) is closed Element of bool the carrier of T

Fr Z9 is closed Element of bool the carrier of T

T is non empty TopSpace-like discrete V130() V131() V132() TopStruct

[#] T is non empty non proper open closed dense non boundary Element of bool the carrier of T

the carrier of T is non empty set

bool the carrier of T is non empty set

card ([#] T) is non empty ordinal cardinal set

density T is ordinal cardinal set

A is open closed Element of bool the carrier of T

card A is ordinal cardinal set

T is non empty TopSpace-like discrete V130() V131() V132() TopStruct

[#] T is non empty non proper open closed dense non boundary Element of bool the carrier of T

the carrier of T is non empty set

bool the carrier of T is non empty set

card ([#] T) is non empty ordinal cardinal 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

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

T is set

bool T is non empty set

bool (bool T) is non empty set

T is set

bool T is non empty set

bool (bool T) is non empty set

A is Element of bool (bool T)

F is countable Element of bool (bool T)

union F is Element of bool T

T is set

bool T is non empty set

bool (bool T) is non empty set

A is non empty V21() V22() V23() compl-closed sigma-multiplicative sigma-additive Element of bool (bool T)

T is set

bool T is non empty set

bool (bool T) is non empty set

A is Element of bool (bool T)

F is countable Element of bool (bool T)

T is set

bool T is non empty set

bool (bool T) is non empty set

A is Element of bool (bool T)

T is set

bool T is non empty set

bool (bool T) is non empty set

A is Element of bool (bool T)

F is non empty countable Element of bool (bool T)

union F is Element of bool T

F is non empty V21() V22() V23() compl-closed sigma-multiplicative sigma-additive (T) Element of bool (bool T)

T is set

bool T is non empty set

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

bool (bool the carrier of T) is non empty set

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

F is Element of bool the carrier of T

F ` is Element of bool the carrier of T

the carrier of T \ F is set

(F `) ` is Element of bool the carrier of T

the carrier of T \ (F `) is set

F is Element of bool the carrier of T

F ` is Element of bool the carrier of T

the carrier of T \ F is set

(F `) ` is Element of bool the carrier of T

the carrier of T \ (F `) is set

T is set

bool T is non empty set

bool (bool T) is non empty set

A is Element of bool (bool T)

COMPLEMENT A is Element of bool (bool T)

F is set

Z is Element of bool T

Z ` is Element of bool T

T \ Z is set

F is set

Z is Element of bool T

Z ` is Element of bool T

T \ Z is set

(Z `) ` is Element of bool T

T \ (Z `) is set

T is set

bool T is non empty set

bool (bool T) is non empty set

A is Element of bool (bool T)

F is Element of bool (bool T)

COMPLEMENT A is Element of bool (bool T)

Z is set

Z9 is Element of bool T

Z9 ` is Element of bool T

T \ Z9 is set

(Z9 `) ` is Element of bool T

T \ (Z9 `) is set

T is set

bool T is non empty set

bool (bool T) is non empty set

A is Element of bool (bool T)

F is countable Element of bool (bool T)

union F is Element of bool T

Z is non empty Element of bool (bool T)

COMPLEMENT Z is non empty Element of bool (bool T)

meet (COMPLEMENT Z) is Element of bool T

(meet (COMPLEMENT Z)) ` is Element of bool T

T \ (meet (COMPLEMENT Z)) is set

union Z is Element of bool T

(union Z) ` is Element of bool T

T \ (union Z) is set

((union Z) `) ` is Element of bool T

T \ ((union Z) `) is set

F is countable Element of bool (bool T)

meet F is Element of bool T

Z is non empty Element of bool (bool T)

COMPLEMENT Z is non empty Element of bool (bool T)

union (COMPLEMENT Z) is Element of bool T

(union (COMPLEMENT Z)) ` is Element of bool T

T \ (union (COMPLEMENT Z)) is set

meet Z is Element of bool T

(meet Z) ` is Element of bool T

T \ (meet Z) is set

((meet Z) `) ` is Element of bool T

T \ ((meet 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

bool (bool the carrier of T) is non empty set

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

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

T is set

bool T is non empty set

bool (bool T) is non empty set

A is countable Element of bool (bool T)

COMPLEMENT A is Element of bool (bool 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

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

F is Element of bool the carrier of T

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

bool (bool the carrier of T) is non empty set

{} (bool the carrier of T) is empty proper ordinal natural finite V40() cardinal {} -element countable open closed Element of bool (bool the carrier of T)

T is set

bool T is non empty set

bool (bool T) is non empty set

{} (bool T) is empty proper ordinal natural finite V40() cardinal {} -element countable Element of bool (bool T)

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 set

bool (bool the carrier of T) is non empty set

A is Element of bool the carrier of T

{A} is non empty trivial finite 1 -element countable Element of bool (bool the carrier of T)

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

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

bool (bool the carrier of T) is non empty set

A is Element of bool the carrier of T

{A} is non empty trivial finite 1 -element countable Element of bool (bool the carrier of T)

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

Z is Element of bool the carrier of T

T is set

bool T is non empty set

bool (bool T) is non empty set

A is Element of bool (bool T)

F is Element of bool (bool T)

INTERSECTION (A,F) is set

Z is set

Z9 is set

Y is set

Z9 /\ Y is set

UNION (A,F) is set

Z is set

Z9 is set

Y is set

Z9 \/ Y 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

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

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

( the carrier of T,A,F) is Element of bool (bool the carrier of T)

Z is Element of bool the carrier of T

Z9 is set

Y is set

Z9 /\ Y is set

Z is Element of bool the carrier of T

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

bool (bool the carrier of T) is non empty set

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

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

( the carrier of T,A,F) is Element of bool (bool the carrier of T)

Z is Element of bool the carrier of T

Z9 is set

Y is set

Z9 \/ Y is set

Z is Element of bool the carrier of T

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

bool (bool the carrier of T) is non empty set

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

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

( the carrier of T,A,F) is Element of bool (bool the carrier of T)

Z is Element of bool the carrier of T

Z9 is set

Y is set

Z9 /\ Y is set

Z is Element of bool the carrier of T

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

bool (bool the carrier of T) is non empty set

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

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

( the carrier of T,A,F) is Element of bool (bool the carrier of T)

Z is Element of bool the carrier of T

Z9 is set

Y is set

Z9 \/ Y is set

Z is Element of bool the carrier of T

Z is Element of bool the carrier of T

T is set

bool T is non empty set

bool (bool T) is non empty set

A is Element of bool (bool T)

F is Element of bool (bool T)

(T,A,F) is Element of bool (bool T)

card (T,A,F) is ordinal cardinal set

[:A,F:] is set

card [:A,F:] is ordinal cardinal set

[:(bool T),(bool T):] is non empty set

{ H

a is set

X is Element of [:(bool T),(bool T):]

X `1 is set

X `2 is set

(X `1) /\ (X `2) is set

X `1 is Element of bool T

X `2 is Element of bool T

a is set

X is set

Y is set

X /\ Y is set

X is Element of bool T

Y is Element of bool T

[X,Y] is V15() Element of [:(bool T),(bool T):]

{X,Y} is finite countable set

{X} is non empty trivial finite 1 -element countable set

{{X,Y},{X}} is finite V40() countable set

[X,Y] `1 is Element of bool T

[X,Y] `2 is Element of bool T

card { H

T is set

bool T is non empty set

bool (bool T) is non empty set

A is Element of bool (bool T)

F is Element of bool (bool T)

(T,A,F) is Element of bool (bool T)

card (T,A,F) is ordinal cardinal set

[:A,F:] is set

card [:A,F:] is ordinal cardinal set

[:(bool T),(bool T):] is non empty set

{ H

a is set

X is Element of [:(bool T),(bool T):]

X `1 is set

X `2 is set

(X `1) \/ (X `2) is set

X `1 is Element of bool T

X `2 is Element of bool T

a is set

X is set

Y is set

X \/ Y is set

X is Element of bool T

Y is Element of bool T

[X,Y] is V15() Element of [:(bool T),(bool T):]

{X,Y} is finite countable set

{X} is non empty trivial finite 1 -element countable set

{{X,Y},{X}} is finite V40() countable set

[X,Y] `1 is Element of bool T

[X,Y] `2 is Element of bool T

card { H

T is set

A is set

UNION (T,A) is set

union (UNION (T,A)) is set

union T is set

union A is set

(union T) \/ (union A) is set

F is set

Z is set

Z9 is set

Y is set

Z9 \/ Y is set

T is set

A is set

union T is set

union A is set

(union T) \/ (union A) is set

UNION (T,A) is set

union (UNION (T,A)) is set

F is set

Z is set

Z9 is set

Z9 \/ Z is set

Z is set

Z9 is set

Z \/ Z9 is set

T is set

UNION ({},T) is set

A is set

F is set

Z is set

F \/ Z is set

T is set

A is set

UNION (T,A) is set

F is set

Z is set

F \/ Z is set

T is set

A is set

INTERSECTION (T,A) is set

F is set

Z is set

F /\ Z is set

T is set

A is set

UNION (T,A) is set

meet (UNION (T,A)) is set

meet T is set

meet A is set

(meet T) \/ (meet A) is set

F is set

Z is set

Z9 is set

Z \/ Z9 is set

T is set

A is set

UNION (T,A) is set

meet (UNION (T,A)) is set

meet T is set

meet A is set

(meet T) \/ (meet A) is set

T is set

A is set

meet T is set

meet A is set

(meet T) /\ (meet A) is set

INTERSECTION (T,A) is set

meet (INTERSECTION (T,A)) is set

F is set

Z is set

Z9 is set

Y is set

F /\ Y is set

Y is set

Y /\ Z is set

F /\ Z is set

Z9 is set

Y is set

Z is set

Z is set

Z /\ Z is set

T is TopSpace-like TopStruct

the carrier of T is set

bool the carrier of T is non empty set

T is TopSpace-like TopStruct

the carrier of T is set

bool the carrier of T 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

A is Element of bool the carrier of T

{} T is empty proper ordinal natural finite V40() cardinal {} -element countable open closed boundary nowhere_dense V124(T) V127(T) dense-in-itself perfect scattered Element of bool the carrier of T

bool (bool the carrier of T) is non empty set

F is empty proper ordinal natural finite V40() cardinal {} -element countable open closed Element of bool (bool the carrier of T)

union F is finite countable V127(T) Element of bool the carrier of T

bool (bool the carrier of T) is non empty set

{({} T)} is non empty trivial finite V40() 1 -element countable Element of bool (bool the carrier of T)

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

meet F is Element of bool the carrier of T

T is non empty TopSpace-like TopStruct

[#] T is non empty non proper open closed dense non boundary Element of bool the carrier of T

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

{([#] T)} is non empty trivial finite 1 -element countable Element of bool (bool the carrier of T)

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

union A is Element of bool the carrier of T

T is non empty TopSpace-like TopStruct

[#] T is non empty non proper open closed dense non boundary Element of bool the carrier of T

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

{([#] T)} is non empty trivial finite 1 -element countable Element of bool (bool the carrier of T)

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

meet A is Element of bool the carrier of T

T is non empty TopSpace-like TopStruct

[#] T is non empty non proper open closed dense non boundary Element of bool the carrier of T

the carrier of T is non empty set

bool the carrier of T 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

A is Element of bool the carrier of T

A ` is Element of bool the carrier of T

the carrier of T \ A is set

bool (bool the carrier of T) is non empty set

F is countable closed Element of bool (bool the carrier of T)

union F is Element of bool the carrier of T

COMPLEMENT F is countable Element of bool (bool the carrier of T)

(union F) ` is Element of bool the carrier of T

the carrier of T \ (union F) is set

meet (COMPLEMENT F) is Element of bool the carrier of T

[#] T is non empty non proper open closed dense non boundary (T) (T) 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

A is Element of bool the carrier of T

A ` is Element of bool the carrier of T

the carrier of T \ A is set

bool (bool the carrier of T) is non empty set

F is countable open Element of bool (bool the carrier of T)

meet F is Element of bool the carrier of T

COMPLEMENT F is countable Element of bool (bool the carrier of T)

(meet F) ` is Element of bool the carrier of T

the carrier of T \ (meet F) is set

union (COMPLEMENT F) is Element of bool the carrier of T

[#] T is non empty non proper open closed dense non boundary (T) (T) 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

A is Element of bool the carrier of T

F is Element of bool the carrier of T

A /\ F is Element of bool the carrier of T

bool (bool the carrier of T) is non empty set

Z is countable closed Element of bool (bool the carrier of T)

union Z is Element of bool the carrier of T

Z9 is countable closed Element of bool (bool the carrier of T)

union Z9 is Element of bool the carrier of T

( the carrier of T,Z,Z9) is Element of bool (bool the carrier of T)

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

card Y is ordinal cardinal set

[:Z,Z9:] is set

card [:Z,Z9:] is ordinal cardinal set

union 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 set

A is Element of bool the carrier of T

F is Element of bool the carrier of T

A \/ F is Element of bool the carrier of T

bool (bool the carrier of T) is non empty set

Z is countable closed Element of bool (bool the carrier of T)

union Z is Element of bool the carrier of T

Z9 is countable closed Element of bool (bool the carrier of T)

union Z9 is Element of bool the carrier of T

( the carrier of T,Z,Z9) is Element of bool (bool the carrier of T)

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

card Y is ordinal cardinal set

[:Z,Z9:] is set

card [:Z,Z9:] is ordinal cardinal set

union 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 set

A is Element of bool the carrier of T

F is Element of bool the carrier of T

A \/ F is Element of bool the carrier of T

bool (bool the carrier of T) is non empty set

Z is countable open Element of bool (bool the carrier of T)

meet Z is Element of bool the carrier of T

Z9 is countable open Element of bool (bool the carrier of T)

meet Z9 is Element of bool the carrier of T

( the carrier of T,Z,Z9) is Element of bool (bool the carrier of T)

meet ( the carrier of T,Z,Z9) is Element of bool the carrier of T

(meet Z) \/ (meet Z9) is Element of bool the carrier of T

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

meet Y is Element of bool the carrier of T

card Y is ordinal cardinal set

[:Z,Z9:] is set

card [:Z,Z9:] is ordinal cardinal 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

A is Element of bool the carrier of T

F is Element of bool the carrier of T

A /\ F is Element of bool the carrier of T

bool (bool the carrier of T) is non empty set

Z is countable open Element of bool (bool the carrier of T)

meet Z is Element of bool the carrier of T

Z9 is countable open Element of bool (bool the carrier of T)

meet Z9 is Element of bool the carrier of T

( the carrier of T,Z,Z9) is Element of bool (bool the carrier of T)

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

card Y is ordinal cardinal set

[:Z,Z9:] is set

card [:Z,Z9:] is ordinal cardinal set

meet Y is Element of bool the carrier of T

{} T is empty proper ordinal natural finite V40() cardinal {} -element countable open closed boundary nowhere_dense V124(T) V127(T) dense-in-itself perfect scattered (T) (T) 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

A is Element of bool the carrier of T

bool (bool the carrier of T) is non empty set

{A} is non empty trivial finite 1 -element countable Element of bool (bool the carrier of T)

F is countable closed Element of bool (bool the carrier of T)

union 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

A is Element of bool the carrier of T

bool (bool the carrier of T) is non empty set

{A} is non empty trivial finite 1 -element countable Element of bool (bool the carrier of T)

F is countable open Element of bool (bool the carrier of T)

meet F is Element of bool the carrier of T

bool the carrier of R^1 is non empty set

T is Element of bool the carrier of R^1

bool RAT is non empty non trivial non finite set

A is set

A is set

F is set

bool (bool the carrier of R^1) is non empty set

F is Element of bool (bool the carrier of R^1)

union F is Element of bool the carrier of R^1

Z is Element of bool the carrier of R^1

Z9 is Element of RAT

{Z9} is non empty trivial finite 1 -element countable Element of bool RAT

{ {b

Z is set

Z9 is Element of RAT

{Z9} is non empty trivial finite 1 -element countable Element of bool RAT

Z is set

Z9 is Element of RAT

{Z9} is non empty trivial finite 1 -element countable Element of bool RAT

Y is Element of RAT

Z is set

Z9 is Element of RAT

{Z9} is non empty trivial finite 1 -element countable Element of bool RAT

Z is set

Z9 is set

Y is Element of RAT

{Y} is non empty trivial finite 1 -element countable Element of bool RAT

Z is Element of bool (bool the carrier of R^1)

union Z is Element of bool the carrier of R^1

T is TopSpace-like TopStruct

the carrier of T is set

bool the carrier of T is non empty set

A is Element of bool the carrier of T

Der A is Element of bool the carrier of T

Cl (Der A) is closed Element of bool the carrier of T

T is non empty TopSpace-like TopStruct

the carrier of T is non empty set

A is Element of the carrier of T

F is Element of the carrier of T

{F} is non empty trivial finite 1 -element countable V127(T) Element of bool the carrier of T

bool the carrier of T is non empty set

Cl {F} is closed Element of bool the carrier of T

{A} is non empty trivial finite 1 -element countable V127(T) Element of bool the carrier of T

Cl {A} is closed Element of bool the carrier of T

Der {A} is Element of bool the carrier of T

(Der {A}) ` is Element of bool the carrier of T

the carrier of T \ (Der {A}) is set

the a_neighborhood of A is a_neighborhood of A

Y is Element of bool the carrier of T

{A} /\ Y is finite countable V127(T) Element of bool the carrier of T

Z is Element of the carrier of T

Z9 is open Element of bool the carrier of T

{A} /\ Z9 is finite countable V127(T) Element of bool the carrier of T

Z is Element of bool the carrier of T

T is TopSpace-like TopStruct

A is non empty TopSpace-like TopStruct

A is empty trivial finite {} -element TopSpace-like T_0 T_1 T_2 V126() second-countable V259() countable separable TopStruct

T is TopSpace-like TopStruct

T is non empty TopSpace-like TopStruct

the carrier of T is non empty set

bool the carrier of T 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

A is Element of bool the carrier of T

F is Element of bool the carrier of T

Z is Element of the carrier of T

Z9 is a_neighborhood of Z

Z9 /\ F is Element of bool the carrier of T

Z9 /\ A 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

A is Element of bool the carrier of T

F is Element of bool the carrier of T

F is Element of bool the carrier of T

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

A is Element of bool the carrier of T

F is Element of the carrier of T

Z is open Element of bool the carrier of T

Z9 is a_neighborhood of F

Z9 /\ A is Element of bool the carrier of T

Y is non empty non trivial non finite non countable set

Z is Element of Y

Z is Element of 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

A is Element of bool the carrier of T

(T,A) is Element of bool the carrier of T

Der A is Element of bool the carrier of T

F is set

Z is Element of 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

A is Element of bool the carrier of T

(T,A) is Element of bool the carrier of T

Cl (T,A) is closed Element of bool the carrier of T

F is set

Z is Element of the carrier of T

Z9 is a_neighborhood of Z

Z9 /\ A is Element of bool the carrier of T

Y is Element of bool the carrier of T

Z is set

Z is Element of the carrier of T

N1 is a_neighborhood of Z

N1 /\ A 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

A is Element of bool the carrier of T

(T,A) is Element of bool the carrier of T

F is Element of bool the carrier of T

(T,F) is Element of bool the carrier of T

Z is set

Z9 is Element of 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

A is Element of bool the carrier of T

F is Element of bool the carrier of T

A \/ F is Element of bool the carrier of T

Z is Element of the carrier of T

Z9 is a_neighborhood of Z

Z9 /\ A is Element of bool the carrier of T

Y is a_neighborhood of Z

Y /\ F is Element of bool the carrier of T

Z9 /\ Y is Element of bool the carrier of T

Z is a_neighborhood of Z

Z /\ A is Element of bool the carrier of T

Z /\ F is Element of bool the carrier of T

(Z /\ A) \/ (Z /\ F) is Element of bool the carrier of T

Z /\ (A \/ 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

A is Element of bool the carrier of T

(T,A) is Element of bool the carrier of T

F is Element of bool the carrier of T

A \/ F is Element of bool the carrier of T

(T,(A \/ F)) is Element of bool the carrier of T

(T,F) is Element of bool the carrier of T

(T,A) \/ (T,F) is Element of bool the carrier of T

Z is set

Z9 is Element of 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

A is Element of bool the carrier of T

F is Element of the carrier of T

the a_neighborhood of F is a_neighborhood of F

the a_neighborhood of F /\ A 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

A is Element of bool the carrier of T

(T,A) is Element of bool the carrier of T

F is set

Z is Element of 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

A is countable Element of bool the carrier of T

(T,A) 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

bool (bool the carrier of T) is non empty set

the open V253(T) Element of bool (bool the carrier of T) is open V253(T) Element of bool (bool the carrier of T)

weight T is ordinal cardinal set

F is open V253(T) Element of bool (bool the carrier of T)

card F is ordinal cardinal set

card (card F) is ordinal cardinal set

card omega is non trivial ordinal non finite cardinal set

the non empty finite TopSpace-like V126() second-countable V259() countable separable TopStruct is non empty finite TopSpace-like V126() second-countable V259() countable separable TopStruct

T is non empty TopSpace-like TopStruct

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

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

A is Element of bool the carrier of T

A is Element of bool the carrier of T

A ` is Element of bool the carrier of T

the carrier of T \ A is set

A is countable Element of bool (bool the carrier of T)

union A 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

[:NAT,(bool T):] is non trivial non finite set

bool [:NAT,(bool T):] is non empty non trivial non finite set

A is Relation-like NAT -defined bool T -valued Function-like V18( NAT , bool T) Element of bool [:NAT,(bool T):]

rng A is Element of bool (bool T)

A . 1 is set

card (rng A) is ordinal cardinal set

proj1 A is set

card (proj1 A) is ordinal cardinal set

F is non empty Element of bool (bool 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

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

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

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

bool (bool the carrier of T) is non empty set

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

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

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

bool (bool the carrier of T) is non empty set

(T) is non empty compl-closed (T) (T) ( the carrier of T) ( the carrier of T) Element of bool (bool the carrier of T)

T is non empty TopSpace-like TopStruct

the carrier of T is non empty set

(T) is non empty compl-closed (T) (T) ( the carrier of T) ( the carrier of T) Element of bool (bool the carrier of T)

bool the carrier of T is non empty set

bool (bool the carrier of T) is non empty set

sigma (T) is non empty V21() V22() V23() compl-closed sigma-multiplicative sigma-additive ( the carrier of T) Element of bool (bool the carrier of T)

T is non empty TopSpace-like TopStruct

the carrier of T is non empty set

(T) is non empty compl-closed (T) (T) ( the carrier of T) ( the carrier of T) Element of bool (bool the carrier of T)

bool the carrier of T is non empty set

bool (bool the carrier of T) is non empty set

sigma (T) is non empty V21() V22() V23() compl-closed sigma-multiplicative sigma-additive ( the carrier of T) Element of bool (bool the carrier of T)

T is non empty 1-sorted

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

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

sigma (T) is non empty V21() V22() V23() compl-closed sigma-multiplicative sigma-additive ( the carrier of T) 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

A is non empty V21() V22() V23() compl-closed sigma-multiplicative sigma-additive ( the carrier of T) 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

A 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 set

bool (bool the carrier of T) is non empty set

(T) is non empty compl-closed (T) (T) ( the carrier of T) ( the carrier of T) Element of bool (bool the carrier of T)

sigma (T) is non empty V21() V22() V23() compl-closed compl-closed sigma-multiplicative sigma-multiplicative sigma-additive sigma-additive (T) (T) ( the carrier of T) ( the carrier of T) Element of bool (bool the carrier of T)

T is non empty TopSpace-like TopStruct

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

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)

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

bool (bool the carrier of T) is non empty set

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

{ b

meet { b

Z9 is set

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

(T) is non empty compl-closed (T) (T) ( the carrier of T) ( the carrier of T) Element of bool (bool the carrier of T)

Z9 is Element of bool the carrier of T

Z9 ` is Element of bool the carrier of T

the carrier of T \ Z9 is set

Y is set

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

bool the carrier of T is non empty Element of bool (bool the carrier of T)

[:NAT,(bool the carrier of T):] is non trivial non finite set

bool [:NAT,(bool the carrier of T):] is non empty non trivial non finite set

Z9 is Relation-like NAT -defined bool the carrier of T -valued Function-like V18( NAT , bool the carrier of T) Element of bool [:NAT,(bool the carrier of T):]

rng Z9 is Element of bool (bool the carrier of T)

Intersection Z9 is Element of bool the carrier of T

Y is set

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

Z is ordinal natural finite cardinal countable set

Z9 . Z is set

Z9 is set

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

Z9 is non empty V21() V22() V23() compl-closed sigma-multiplicative sigma-additive ( the carrier of T) Element of bool (bool the carrier of T)

Y is Element of bool the carrier of T

Z is set

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

Y is non empty compl-closed (T) (T) ( the carrier of T) ( the carrier of T) Element of bool (bool the carrier of T)

Z is set

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

Z is non empty compl-closed (T) (T) ( the carrier of T) ( the carrier of T) 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

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

F is non empty compl-closed (T) (T) ( the carrier of T) ( the carrier of T) Element of bool (bool the carrier of T)

Z is non empty compl-closed (T) (T) ( the carrier of T) ( the carrier of T) Element of bool (bool the carrier of T)

A is non empty compl-closed (T) (T) ( the carrier of T) ( the carrier of T) Element of bool (bool the carrier of T)

F is non empty compl-closed (T) (T) ( the carrier of T) ( the carrier of T) 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

(T) is non empty compl-closed (T) (T) ( the carrier of T) ( the carrier of T) Element of bool (bool the carrier of T)

A is closed Element of bool (bool the carrier of T)

F is set

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

bool (bool the carrier of T) is non empty set

(T) is non empty compl-closed (T) (T) ( the carrier of T) ( the carrier of T) Element of bool (bool the carrier of T)

A is open Element of bool (bool the carrier of T)

F is set

Z is Element of bool the carrier of T

T is non empty TopSpace-like TopStruct

(T) is non empty compl-closed (T) (T) ( the carrier of T) ( the carrier of T) Element of bool (bool the carrier of T)

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

Topology_of T is open (T) Element of bool (bool the carrier of T)

the topology of T is non empty open Element of bool (bool the carrier of T)

sigma (Topology_of T) is non empty V21() V22() V23() compl-closed compl-closed sigma-multiplicative sigma-multiplicative sigma-additive ( the carrier of T) Element of bool (bool the carrier of T)

A is non empty V21() V22() V23() compl-closed sigma-multiplicative sigma-additive ( the carrier of T) Element of bool (bool the carrier of T)

Z is set

Z9 is non empty V21() V22() V23() compl-closed sigma-multiplicative sigma-additive ( the carrier of T) 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

T is non empty TopSpace-like TopStruct

the carrier of T is non empty set

bool the carrier of T is non empty set

A is Element of bool the carrier of T

bool (bool the carrier of T) is non empty set

F is countable closed Element of bool (bool the carrier of T)

union F is Element of bool the carrier of T

(T) is non empty compl-closed (T) (T) ( the carrier of T) ( the carrier of T) 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

A is Element of bool the carrier of T

bool (bool the carrier of T) is non empty set

F is countable open Element of bool (bool the carrier of T)

meet F is Element of bool the carrier of T

(T) is non empty compl-closed (T) (T) ( the carrier of T) ( the carrier of T) Element of bool (bool the carrier of T)