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
{ {b1} where b1 is Element of RAT : P1[b1] } is set
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
{ 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
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
{ 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
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
{ 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 Z9 is ordinal cardinal set
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
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
{ 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
card [:A,F:] is ordinal cardinal 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
(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
{ {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
{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)
{ 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)
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)