:: TOPGEN_4 semantic presentation

REAL is non empty non trivial non finite set

bool REAL is non empty non trivial non finite set
ExtREAL is non empty set
is non trivial non finite set
bool is non empty non trivial non finite set
bool ExtREAL is non empty set

bool omega is non empty non trivial non finite set
is non trivial non finite set
bool is non empty non trivial non finite set
bool () 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
is non empty non trivial non finite set
is non empty non trivial non finite set
bool 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()

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

proj1 A is set
proj2 A is set
{ {b1} where b1 is Element of RAT : P1[b1] } is set

proj1 T is set
proj2 T is set
A is set
F is Element of 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
{ b1 where b1 is Element of the carrier of T : b1 in Cl (A \ {b1}) } is set
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

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
{ b1 where b1 is Element of bool the carrier of T : ( b1 in A & b1 c= F ) } is set
union { b1 where b1 is Element of bool the carrier of T : ( b1 in A & b1 c= F ) } is set
Z9 is set
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
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)

{ H1(b1) where b1 is Element of bool the carrier of T : ( b1 in F & S1[b1] ) } is set
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 { H1(b1) where b1 is Element of bool the carrier of T : ( b1 in F & S1[b1] ) } 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

A is Element of bool the carrier of T

T is non empty TopSpace-like TopStruct

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

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 () 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 () 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
() ` is Element of bool the carrier of T
the carrier of T \ () is set
Cl (() `) is closed Element of bool the carrier of T
(Cl ()) /\ (Cl (() `)) 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

A is open 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
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 () is Element of bool T
(meet ()) ` is Element of bool T
T \ (meet ()) is set
union Z is Element of bool T
() ` is Element of bool T
T \ () is set
(() `) ` is Element of bool T
T \ (() `) 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 () is Element of bool T
(union ()) ` is Element of bool T
T \ (union ()) 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)

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

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

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

[:(bool T),(bool T):] is non empty set
{ H1(b1) where b1 is Element of [:(bool T),(bool T):] : b1 in [:A,F:] } is set
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 { H1(b1) where b1 is Element of [:(bool T),(bool T):] : b1 in [:A,F:] } is ordinal cardinal 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)
(T,A,F) is Element of bool (bool T)
card (T,A,F) is ordinal cardinal set
[:A,F:] is set

[:(bool T),(bool T):] is non empty set
{ H1(b1) where b1 is Element of [:(bool T),(bool T):] : b1 in [:A,F:] } is set
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 { H1(b1) where b1 is Element of [:(bool T),(bool T):] : b1 in [:A,F:] } is ordinal cardinal set
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
() \/ () 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
() \/ () 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

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

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

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

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

[:Z,Z9:] is 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)

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

[:Z,Z9:] 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
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)

[:Z,Z9:] is set

meet 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
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
{ {b1} where b1 is Element of RAT : S1[b1] } is set
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

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

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

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

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

card omega is non trivial ordinal non finite cardinal set

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

rng A is Element of bool (bool T)
A . 1 is set

proj1 A is 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)
{ b1 where b1 is Element of bool (bool the carrier of T) : ( A c= b1 & b1 is non empty compl-closed (T) (T) ( the carrier of T) ( the carrier of T) Element of bool (bool the carrier of T) ) } is set
meet { b1 where b1 is Element of bool (bool the carrier of T) : ( A c= b1 & b1 is non empty compl-closed (T) (T) ( the carrier of T) ( the carrier of T) Element of bool (bool the carrier of T) ) } is set
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)

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