REAL is non empty non trivial non finite V84() V85() V86() V90() set
NAT is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal V84() V85() V86() V87() V88() V89() V90() Element of bool REAL
bool REAL is non empty non trivial non finite set
omega is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal V84() V85() V86() V87() V88() V89() V90() set
RAT+ is set
bool RAT+ is non empty set
bool (bool RAT+) is non empty set
DEDEKIND_CUTS is Element of bool (bool RAT+)
REAL+ is set
COMPLEX is non empty non trivial non finite V84() V90() set
bool omega is non empty non trivial non finite set
[:NAT,REAL:] is non empty non trivial V37() V38() V39() 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
bool NAT is non empty non trivial non finite set
RAT is non empty non trivial non finite V84() V85() V86() V87() V90() set
INT is non empty non trivial non finite V84() V85() V86() V87() V88() V90() set
{} is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V28() real ext-real finite V51() cardinal {} -element integer rational V84() V85() V86() V87() V88() V89() V90() set
the empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V28() real ext-real finite V51() cardinal {} -element integer rational V84() V85() V86() V87() V88() V89() V90() set is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V28() real ext-real finite V51() cardinal {} -element integer rational V84() V85() V86() V87() V88() V89() V90() set
1 is non empty epsilon-transitive epsilon-connected ordinal natural V28() real ext-real positive finite cardinal integer rational V84() V85() V86() V87() V88() V89() Element of NAT
0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V28() real ext-real finite V51() cardinal {} -element integer rational V84() V85() V86() V87() V88() V89() V90() Element of NAT
2 is non empty epsilon-transitive epsilon-connected ordinal natural V28() real ext-real positive finite cardinal integer rational V84() V85() V86() V87() V88() V89() Element of NAT
len omega is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal set
{{}} is non empty trivial finite V51() 1 -element V84() V85() V86() V87() V88() V89() set
[:{{}},REAL+:] is set
REAL+ \/ [:{{}},REAL+:] is set
[{},{}] is set
{{},{}} is non empty finite V51() V84() V85() V86() V87() V88() V89() set
{{{},{}},{{}}} is non empty finite V51() set
{[{},{}]} is non empty trivial finite 1 -element set
(REAL+ \/ [:{{}},REAL+:]) \ {[{},{}]} is Element of bool (REAL+ \/ [:{{}},REAL+:])
bool (REAL+ \/ [:{{}},REAL+:]) is non empty set
[:{{}},RAT+:] is set
RAT+ \/ [:{{}},RAT+:] is set
(RAT+ \/ [:{{}},RAT+:]) \ {[{},{}]} is Element of bool (RAT+ \/ [:{{}},RAT+:])
bool (RAT+ \/ [:{{}},RAT+:]) is non empty set
[:{{}},omega:] is non empty non trivial RAT -valued INT -valued V37() V38() V39() V40() non finite set
omega \/ [:{{}},omega:] is non empty set
(omega \/ [:{{}},omega:]) \ {[{},{}]} is Element of bool (omega \/ [:{{}},omega:])
bool (omega \/ [:{{}},omega:]) is non empty set
omega *` omega is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal set
RAT+ \/ DEDEKIND_CUTS is set
{} is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V28() real ext-real finite V51() cardinal {} -element integer rational V84() V85() V86() V87() V88() V89() V90() Element of RAT+
{ { b2 where b2 is Element of RAT+ : not b1 <=' b2 } where b1 is Element of RAT+ : not b1 = {} } is set
(RAT+ \/ DEDEKIND_CUTS) \ { { b2 where b2 is Element of RAT+ : not b1 <=' b2 } where b1 is Element of RAT+ : not b1 = {} } is Element of bool (RAT+ \/ DEDEKIND_CUTS)
bool (RAT+ \/ DEDEKIND_CUTS) is non empty set
K560({}) is M27( {} )
-infty is non real set
+infty is non real set
BB is set
bool BB is non empty set
bool (bool BB) is non empty set
BB is set
bool BB is non empty set
bool (bool BB) is non empty set
X is Element of bool (bool BB)
union X is Element of bool BB
T is set
a is set
a is Element of bool BB
A1 is Element of bool BB
T is set
a is Element of bool BB
BB is set
bool BB is non empty set
bool (bool BB) is non empty set
X is Element of bool (bool BB)
UniCl X is Element of bool (bool BB)
T is TopStruct
the carrier of T is set
the topology of T is Element of bool (bool the carrier of T)
bool the carrier of T is non empty set
bool (bool the carrier of T) is non empty set
union X is Element of bool BB
a is Element of bool (bool the carrier of T)
union a is Element of bool the carrier of T
UniCl the topology of T is Element of bool (bool the carrier of T)
a is Element of bool the carrier of T
a is Element of bool the carrier of T
a /\ a is Element of bool the carrier of T
{ b1 where b1 is Element of bool the carrier of T : ( b1 in X & b1 c= a /\ a ) } is set
bool BB is non empty Element of bool (bool BB)
A2 is set
a is Element of 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
a is Element of bool (bool the carrier of T)
union a is Element of bool the carrier of T
A2 is Element of bool (bool the carrier of T)
union A2 is Element of bool the carrier of T
bool (a /\ a) is non empty Element of bool (bool (a /\ a))
bool (a /\ a) is non empty set
bool (bool (a /\ a)) is non empty set
B is set
C is Element of bool the carrier of T
union (bool (a /\ a)) is Element of bool (a /\ a)
B is set
C is set
y is set
C /\ y is set
C is Element of bool BB
B is set
C is Element of bool the carrier of T
a is Element of bool (bool the carrier of T)
BB is set
bool BB is non empty Element of bool (bool BB)
bool BB is non empty set
bool (bool BB) is non empty set
bool (bool BB) is non empty Element of bool (bool (bool BB))
bool (bool BB) is non empty set
bool (bool (bool BB)) is non empty set
X is Relation-like non-empty BB -defined Function-like V33(BB) set
rng X is set
Union X is set
union (rng X) is set
union (bool (bool BB)) is Element of bool (bool BB)
dom X is Element of bool BB
T is Element of bool (bool BB)
a is set
A1 is set
a is set
a /\ A1 is set
X . a is set
A2 is set
X . A2 is set
A2 is set
a is set
X . a is set
a is set
a /\ A2 is set
a is set
B is Element of bool BB
UniCl T is Element of bool (bool BB)
a is TopStruct
the carrier of a is set
the topology of a is Element of bool (bool the carrier of a)
bool the carrier of a is non empty set
bool (bool the carrier of a) is non empty set
a is set
X . a is set
the Element of X . a is Element of X . a
a is non empty TopSpace-like TopStruct
the carrier of a is non empty set
A1 is non empty Relation-like the carrier of a -defined Function-like V33( the carrier of a) set
A2 is Element of the carrier of a
A1 . A2 is set
bool the carrier of a is non empty set
bool (bool the carrier of a) is non empty set
a is Element of bool (bool the carrier of a)
the topology of a is non empty Element of bool (bool the carrier of a)
a is set
Intersect a is Element of bool the carrier of a
a is Element of bool the carrier of a
B is Element of bool (bool the carrier of a)
union B is Element of bool the carrier of a
C is set
X . A2 is set
y is set
X . y is set
y is set
BB is set
bool BB is non empty set
bool (bool BB) is non empty set
X is Element of bool (bool BB)
COMPLEMENT X is Element of bool (bool BB)
a is TopStruct
the carrier of a is set
the topology of a is Element of bool (bool the carrier of a)
bool the carrier of a is non empty set
bool (bool the carrier of a) is non empty set
{} a is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V28() real ext-real finite V51() cardinal {} -element integer rational V84() V85() V86() V87() V88() V89() V90() boundary Element of bool the carrier of a
({} a) ` is Element of bool the carrier of a
the carrier of a \ ({} a) is set
a is Element of bool (bool the carrier of a)
COMPLEMENT a is Element of bool (bool the carrier of a)
Intersect (COMPLEMENT a) is Element of bool the carrier of a
union a is Element of bool the carrier of a
(union a) ` is Element of bool the carrier of a
the carrier of a \ (union a) is set
a is Element of bool the carrier of a
A1 is Element of bool the carrier of a
a /\ A1 is Element of bool the carrier of a
A1 ` is Element of bool the carrier of a
the carrier of a \ A1 is set
a ` is Element of bool the carrier of a
the carrier of a \ a is set
(a `) \/ (A1 `) is Element of bool the carrier of a
(a /\ A1) ` is Element of bool the carrier of a
the carrier of a \ (a /\ A1) is set
a is Element of bool the carrier of a
a ` is Element of bool the carrier of a
the carrier of a \ a is set
F1() is set
bool F1() is non empty set
bool (bool F1()) is non empty set
{ b1 where b1 is Element of bool F1() : P1[b1] } is set
bool F1() is non empty Element of bool (bool F1())
T is set
a is Element of bool F1()
T is Element of bool (bool F1())
COMPLEMENT T is Element of bool (bool F1())
TopStruct(# F1(),(COMPLEMENT T) #) is strict TopStruct
a is set
A1 is set
a \/ A1 is set
A2 is Element of bool F1()
a is Element of bool F1()
A2 \/ a is Element of bool F1()
a is Element of bool (bool F1())
Intersect a is Element of bool F1()
A1 is set
A2 is Element of bool F1()
a is strict TopSpace-like TopStruct
the carrier of a is set
bool the carrier of a is non empty set
A1 is Element of bool the carrier of a
A2 is Element of bool F1()
A2 is Element of bool F1()
BB is TopSpace-like TopStruct
the carrier of BB is set
bool the carrier of BB is non empty set
X is TopSpace-like TopStruct
the carrier of X is set
bool the carrier of X is non empty set
the topology of BB is non empty Element of bool (bool the carrier of BB)
bool (bool the carrier of BB) is non empty set
the topology of X is non empty Element of bool (bool the carrier of X)
bool (bool the carrier of X) is non empty set
[#] X is non proper open closed dense Element of bool the carrier of X
[#] BB is non proper open closed dense Element of bool the carrier of BB
T is set
a is Element of bool the carrier of BB
a is Element of bool the carrier of X
BB is TopSpace-like TopStruct
the carrier of BB is set
bool the carrier of BB is non empty set
X is TopSpace-like TopStruct
the carrier of X is set
bool the carrier of X is non empty set
the topology of BB is non empty Element of bool (bool the carrier of BB)
bool (bool the carrier of BB) is non empty set
TopStruct(# the carrier of BB, the topology of BB #) is strict TopSpace-like TopStruct
the topology of X is non empty Element of bool (bool the carrier of X)
bool (bool the carrier of X) is non empty set
TopStruct(# the carrier of X, the topology of X #) is strict TopSpace-like TopStruct
BB is TopSpace-like TopStruct
the carrier of BB is set
bool the carrier of BB is non empty set
X is TopSpace-like TopStruct
the carrier of X is set
bool the carrier of X is non empty set
the topology of BB is non empty Element of bool (bool the carrier of BB)
bool (bool the carrier of BB) is non empty set
the topology of X is non empty Element of bool (bool the carrier of X)
bool (bool the carrier of X) is non empty set
[#] X is non proper open closed dense Element of bool the carrier of X
[#] BB is non proper open closed dense Element of bool the carrier of BB
T is set
a is Element of bool the carrier of BB
a is Element of bool the carrier of X
a ` is Element of bool the carrier of X
the carrier of X \ a is set
BB is TopSpace-like TopStruct
the carrier of BB is set
bool the carrier of BB is non empty set
X is TopSpace-like TopStruct
the carrier of X is set
bool the carrier of X is non empty set
the topology of BB is non empty Element of bool (bool the carrier of BB)
bool (bool the carrier of BB) is non empty set
TopStruct(# the carrier of BB, the topology of BB #) is strict TopSpace-like TopStruct
the topology of X is non empty Element of bool (bool the carrier of X)
bool (bool the carrier of X) is non empty set
TopStruct(# the carrier of X, the topology of X #) is strict TopSpace-like TopStruct
BB is set
X is set
bool X is non empty Element of bool (bool X)
bool X is non empty set
bool (bool X) is non empty set
[:BB,(bool X):] is set
bool [:BB,(bool X):] is non empty set
T is Relation-like BB -defined bool X -valued Element of bool [:BB,(bool X):]
rng T is set
BB is set
bool BB is non empty Element of bool (bool BB)
bool BB is non empty set
bool (bool BB) is non empty set
[:(bool BB),(bool BB):] is non empty set
bool [:(bool BB),(bool BB):] is non empty set
X is non empty Relation-like bool BB -defined bool BB -valued Function-like V33( bool BB) V34( bool BB, bool BB) Element of bool [:(bool BB),(bool BB):]
X . {} is set
((bool BB),BB,X) is Element of bool (bool BB)
COMPLEMENT ((bool BB),BB,X) is Element of bool (bool BB)
dom X is Element of bool (bool BB)
bool (bool BB) is non empty set
a is set
a is set
A1 is set
X . A1 is set
A2 is set
X . A2 is set
a \/ a is set
X . a is set
(X . a) \/ a is set
X . a is set
(X . a) \/ (X . a) is set
a is Element of bool BB
X . a is Element of bool BB
a is Element of bool BB
X . a is Element of bool BB
(X . a) \/ (X . a) is Element of bool BB
X . ((X . a) \/ (X . a)) is Element of bool BB
a is Element of bool BB
a is Element of bool BB
a \/ a is Element of bool BB
X . a is Element of bool BB
X . a is Element of bool BB
(X . a) \/ (X . a) is Element of bool BB
a is Element of bool (bool BB)
a is set
Intersect a is Element of bool BB
X . (Intersect a) is Element of bool BB
A1 is Element of bool BB
X . A1 is Element of bool BB
A2 is set
X . A2 is set
a is TopStruct
the carrier of a is set
the topology of a is Element of bool (bool the carrier of a)
bool the carrier of a is non empty set
bool (bool the carrier of a) is non empty set
{} BB is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V28() real ext-real finite V51() cardinal {} -element integer rational V84() V85() V86() V87() V88() V89() V90() Element of bool BB
a is Element of bool the carrier of a
Cl a is Element of bool the carrier of a
X . a is set
A1 is Element of bool BB
X . A1 is Element of bool BB
a is Element of bool the carrier of a
A2 is Element of bool BB
X . A2 is Element of bool BB
a is set
X . a is set
F2({}) is set
F1() is set
bool F1() is non empty set
bool F1() is non empty Element of bool (bool F1())
bool (bool F1()) is non empty set
X is Relation-like Function-like set
dom X is set
T is set
F2(T) is set
X . T is set
[:(bool F1()),(bool F1()):] is non empty set
bool [:(bool F1()),(bool F1()):] is non empty set
T is non empty Relation-like bool F1() -defined bool F1() -valued Function-like V33( bool F1()) V34( bool F1(), bool F1()) Element of bool [:(bool F1()),(bool F1()):]
a is Element of bool F1()
T . a is Element of bool F1()
F2(a) is set
a is Element of bool F1()
a is Element of bool F1()
a \/ a is Element of bool F1()
T . (a \/ a) is Element of bool F1()
T . a is Element of bool F1()
T . a is Element of bool F1()
(T . a) \/ (T . a) is Element of bool F1()
F2(a) is set
F2((a \/ a)) is set
F2(a) is set
a is Element of bool F1()
T . a is Element of bool F1()
T . (T . a) is Element of bool F1()
F2((T . a)) is set
F2(a) is set
T . {} is set
((bool F1()),F1(),T) is Element of bool (bool F1())
COMPLEMENT ((bool F1()),F1(),T) is Element of bool (bool F1())
TopStruct(# F1(),(COMPLEMENT ((bool F1()),F1(),T)) #) is strict TopStruct
a is strict TopSpace-like TopStruct
the carrier of a is set
bool the carrier of a is non empty set
a is Element of bool the carrier of a
Cl a is closed Element of bool the carrier of a
F2(a) is set
T . a is set
BB is TopSpace-like TopStruct
the carrier of BB is set
X is TopSpace-like TopStruct
the carrier of X is set
bool the carrier of BB is non empty set
bool the carrier of X is non empty set
the topology of BB is non empty Element of bool (bool the carrier of BB)
bool (bool the carrier of BB) is non empty set
the topology of X is non empty Element of bool (bool the carrier of X)
bool (bool the carrier of X) is non empty set
T is set
a is closed Element of bool the carrier of BB
Cl a is closed Element of bool the carrier of BB
a is Element of bool the carrier of X
Cl a is closed Element of bool the carrier of X
a is closed Element of bool the carrier of X
Cl a is closed Element of bool the carrier of X
a is Element of bool the carrier of BB
Cl a is closed Element of bool the carrier of BB
TopStruct(# the carrier of BB, the topology of BB #) is strict TopSpace-like TopStruct
TopStruct(# the carrier of X, the topology of X #) is strict TopSpace-like TopStruct
BB is set
bool BB is non empty Element of bool (bool BB)
bool BB is non empty set
bool (bool BB) is non empty set
[:(bool BB),(bool BB):] is non empty set
bool [:(bool BB),(bool BB):] is non empty set
X is non empty Relation-like bool BB -defined bool BB -valued Function-like V33( bool BB) V34( bool BB, bool BB) Element of bool [:(bool BB),(bool BB):]
X . BB is set
((bool BB),BB,X) is Element of bool (bool BB)
a is TopStruct
the carrier of a is set
the topology of a is Element of bool (bool the carrier of a)
bool the carrier of a is non empty set
bool (bool the carrier of a) is non empty set
dom X is Element of bool (bool BB)
bool (bool BB) is non empty set
a is Element of bool the carrier of a
A1 is Element of bool the carrier of a
A2 is set
X . A2 is set
a is set
X . a is set
a /\ A1 is Element of bool the carrier of a
X . a is set
(X . a) /\ A1 is Element of bool the carrier of a
X . A1 is set
(X . a) /\ (X . A1) is set
a is Element of bool BB
X . a is Element of bool BB
B is Element of bool BB
X . B is Element of bool BB
(X . a) /\ (X . B) is Element of bool BB
X . ((X . a) /\ (X . B)) is Element of bool BB
a is Element of bool BB
A1 is Element of bool BB
a /\ A1 is Element of bool BB
X . a is Element of bool BB
X . A1 is Element of bool BB
(X . a) /\ (X . A1) is Element of bool BB
a is Element of bool (bool BB)
A1 is set
A2 is Element of bool BB
X . A2 is Element of bool BB
union a is Element of bool BB
X . (union a) is Element of bool BB
a is set
X . a is set
[#] BB is non proper Element of bool BB
a is Element of bool the carrier of a
Int a is Element of bool the carrier of a
X . a is set
A2 is Element of bool BB
X . A2 is Element of bool BB
a is set
X . a is set
A1 is Element of bool BB
X . A1 is Element of bool BB
a is Element of bool the carrier of a
F1() is set
F2(F1()) is set
bool F1() is non empty set
bool F1() is non empty Element of bool (bool F1())
bool (bool F1()) is non empty set
X is Relation-like Function-like set
dom X is set
T is set
F2(T) is set
X . T is set
[:(bool F1()),(bool F1()):] is non empty set
bool [:(bool F1()),(bool F1()):] is non empty set
T is non empty Relation-like bool F1() -defined bool F1() -valued Function-like V33( bool F1()) V34( bool F1(), bool F1()) Element of bool [:(bool F1()),(bool F1()):]
a is Element of bool F1()
T . a is Element of bool F1()
F2(a) is set
a is Element of bool F1()
a is Element of bool F1()
a /\ a is Element of bool F1()
T . (a /\ a) is Element of bool F1()
T . a is Element of bool F1()
T . a is Element of bool F1()
(T . a) /\ (T . a) is Element of bool F1()
F2(a) is set
F2((a /\ a)) is set
F2(a) is set
a is Element of bool F1()
T . a is Element of bool F1()
T . (T . a) is Element of bool F1()
F2((T . a)) is set
F2(a) is set
T . F1() is set
((bool F1()),F1(),T) is Element of bool (bool F1())
TopStruct(# F1(),((bool F1()),F1(),T) #) is strict TopStruct
a is strict TopSpace-like TopStruct
the carrier of a is set
bool the carrier of a is non empty set
a is Element of bool the carrier of a
Int a is open Element of bool the carrier of a
F2(a) is set
T . a is set
BB is TopSpace-like TopStruct
the carrier of BB is set
X is TopSpace-like TopStruct
the carrier of X is set
bool the carrier of BB is non empty set
bool the carrier of X is non empty set
the topology of BB is non empty Element of bool (bool the carrier of BB)
bool (bool the carrier of BB) is non empty set
the topology of X is non empty Element of bool (bool the carrier of X)
bool (bool the carrier of X) is non empty set
T is Element of bool the carrier of BB
a is Element of bool the carrier of X
T ` is Element of bool the carrier of BB
the carrier of BB \ T is set
Int (T `) is open Element of bool the carrier of BB
a ` is Element of bool the carrier of X
the carrier of X \ a is set
Int (a `) is open Element of bool the carrier of X
Cl T is closed Element of bool the carrier of BB
(Int (a `)) ` is closed Element of bool the carrier of X
the carrier of X \ (Int (a `)) is set
Cl a is closed Element of bool the carrier of X
{ [.b1,b2.[ where b1, b2 is V28() real ext-real Element of REAL : ( not b2 <= b1 & b2 is rational ) } is set
BB is non empty strict TopSpace-like TopStruct
the carrier of BB is non empty set
the topology of BB is non empty Element of bool (bool the carrier of BB)
bool the carrier of BB is non empty set
bool (bool the carrier of BB) is non empty set
T is Element of bool (bool REAL)
UniCl T is Element of bool (bool REAL)
X is non empty strict TopSpace-like TopStruct
the carrier of X is non empty set
the topology of X is non empty Element of bool (bool the carrier of X)
bool the carrier of X is non empty set
bool (bool the carrier of X) is non empty set
a is Element of bool (bool REAL)
UniCl a is Element of bool (bool REAL)
bool REAL is non empty non trivial non finite Element of bool (bool REAL)
X is set
T is V28() real ext-real Element of REAL
a is V28() real ext-real Element of REAL
[.T,a.[ is V84() V85() V86() Element of bool REAL
X is Element of bool (bool REAL)
a is set
a is set
T is set
a /\ a is set
A1 is V28() real ext-real Element of REAL
A2 is V28() real ext-real Element of REAL
[.A1,A2.[ is V84() V85() V86() Element of bool REAL
a is V28() real ext-real Element of REAL
a is V28() real ext-real Element of REAL
[.a,a.[ is V84() V85() V86() Element of bool REAL
max (A1,a) is V28() real ext-real Element of REAL
min (A2,a) is V28() real ext-real Element of REAL
y is V28() real ext-real Element of REAL
[.(max (A1,a)),(min (A2,a)).[ is V84() V85() V86() Element of bool REAL
T is set
a is V28() real ext-real Element of REAL
a + 1 is V28() real ext-real set
a + 0 is V28() real ext-real set
a is V28() real ext-real rational set
[.a,a.[ is V84() V85() V86() Element of bool REAL
A1 is V84() V85() V86() Element of bool REAL
UniCl X is Element of bool (bool REAL)
TopStruct(# REAL,(UniCl X) #) is non empty strict TopStruct
() is non empty strict TopSpace-like TopStruct
the carrier of () is non empty set
the topology of () is non empty Element of bool (bool the carrier of ())
bool the carrier of () is non empty set
bool (bool the carrier of ()) is non empty set
BB is Element of bool (bool REAL)
UniCl BB is Element of bool (bool REAL)
X is V28() real ext-real set
T is V28() real ext-real set
[.X,T.[ is V84() V85() V86() Element of bool REAL
a is Element of the carrier of ()
A1 is V28() real ext-real Element of REAL
A2 is V28() real ext-real rational set
[.X,A2.[ is V84() V85() V86() Element of bool REAL
a is Element of bool the carrier of ()
a is Element of bool the carrier of ()
a is Element of bool the carrier of ()
X is V28() real ext-real set
T is V28() real ext-real set
].X,T.[ is V84() V85() V86() Element of bool REAL
a is Element of the carrier of ()
a is Element of bool the carrier of ()
A1 is V28() real ext-real Element of REAL
A2 is V28() real ext-real rational set
[.A1,A2.[ is V84() V85() V86() Element of bool REAL
a is Element of bool the carrier of ()
a is Element of bool the carrier of ()
X is V28() real ext-real set
left_open_halfline X is V84() V85() V86() Element of bool REAL
K236(-infty,X) is set
a is Element of the carrier of ()
T is Element of bool the carrier of ()
a is V28() real ext-real Element of REAL
{a} is non empty trivial proper finite 1 -element V84() V85() V86() Element of bool REAL
A1 is V28() real ext-real rational set
[.a,A1.[ is V84() V85() V86() Element of bool REAL
A2 is Element of bool the carrier of ()
a is Element of bool the carrier of ()
].a,A1.[ is V84() V85() V86() Element of bool REAL
{a} \/ ].a,A1.[ is non empty V84() V85() V86() Element of bool REAL
X is V28() real ext-real set
right_open_halfline X is V84() V85() V86() Element of bool REAL
K236(X,+infty) is set
a is Element of the carrier of ()
T is Element of bool the carrier of ()
a is V28() real ext-real Element of REAL
{a} is non empty trivial proper finite 1 -element V84() V85() V86() Element of bool REAL
a + 1 is V28() real ext-real set
a + 0 is V28() real ext-real set
A1 is V28() real ext-real rational set
[.a,A1.[ is V84() V85() V86() Element of bool REAL
A2 is Element of bool the carrier of ()
a is Element of bool the carrier of ()
].a,A1.[ is V84() V85() V86() Element of bool REAL
{a} \/ ].a,A1.[ is non empty V84() V85() V86() Element of bool REAL
X is V28() real ext-real set
right_closed_halfline X is V84() V85() V86() Element of bool REAL
K234(X,+infty) is set
a is Element of the carrier of ()
a is V28() real ext-real Element of REAL
a + 1 is V28() real ext-real set
a + 0 is V28() real ext-real set
A1 is V28() real ext-real rational set
[.a,A1.] is V84() V85() V86() Element of bool REAL
{a} is non empty trivial proper finite 1 -element V84() V85() V86() Element of bool REAL
[.a,A1.[ is V84() V85() V86() Element of bool REAL
T is Element of bool the carrier of ()
A2 is Element of bool the carrier of ()
a is Element of bool the carrier of ()
].a,A1.[ is V84() V85() V86() Element of bool REAL
{a} \/ ].a,A1.[ is non empty V84() V85() V86() Element of bool REAL
len INT is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal set
{0} is non empty trivial proper finite V51() 1 -element V84() V85() V86() V87() V88() V89() Element of bool NAT
[:{0},NAT:] is non empty non trivial RAT -valued INT -valued V37() V38() V39() V40() non finite set
NAT \/ [:{0},NAT:] is non empty set
len (NAT \/ [:{0},NAT:]) is non empty epsilon-transitive epsilon-connected ordinal cardinal set
[:NAT,{0}:] is non empty non trivial RAT -valued INT -valued V37() V38() V39() V40() non finite set
len [:NAT,{0}:] is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal set
len [:{0},NAT:] is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal set
len NAT is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal set
omega +` omega is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal set
len RAT is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal set
[:INT,NAT:] is non empty non trivial RAT -valued INT -valued V37() V38() V39() V40() non finite set
X is set
T is set
a is set
[T,a] is set
{T,a} is non empty finite set
{T} is non empty trivial finite 1 -element set
{{T,a},{T}} is non empty finite V51() set
A1 is V28() real ext-real integer rational set
a is epsilon-transitive epsilon-connected ordinal natural V28() real ext-real finite cardinal integer rational set
A1 / a is V28() real ext-real rational Element of COMPLEX
X is Relation-like Function-like set
dom X is set
rng X is set
T is set
a is V28() real ext-real integer rational set
a is V28() real ext-real integer rational set
a / a is V28() real ext-real rational Element of COMPLEX
A1 is epsilon-transitive epsilon-connected ordinal natural V28() real ext-real finite cardinal integer rational V84() V85() V86() V87() V88() V89() Element of NAT
- A1 is V28() real ext-real integer rational set
a / (- A1) is V28() real ext-real rational Element of COMPLEX
a / A1 is V28() real ext-real rational Element of COMPLEX
- (a / A1) is V28() real ext-real rational Element of COMPLEX
- a is V28() real ext-real integer rational set
(- a) / A1 is V28() real ext-real rational Element of COMPLEX
A2 is V28() real ext-real integer rational set
A2 / A1 is V28() real ext-real rational Element of COMPLEX
[A2,A1] is set
{A2,A1} is non empty finite V84() V85() V86() V87() V88() set
{A2} is non empty trivial finite 1 -element V84() V85() V86() V87() V88() set
{{A2,A1},{A2}} is non empty finite V51() set
X . [A2,A1] is set
a is V28() real ext-real integer rational set
a is epsilon-transitive epsilon-connected ordinal natural V28() real ext-real finite cardinal integer rational set
[a,a] is set
{a,a} is non empty finite V84() V85() V86() V87() V88() set
{a} is non empty trivial finite 1 -element V84() V85() V86() V87() V88() set
{{a,a},{a}} is non empty finite V51() set
a / a is V28() real ext-real rational Element of COMPLEX
len [:INT,NAT:] is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal set
[:omega,omega:] is non empty non trivial RAT -valued INT -valued V37() V38() V39() V40() non finite set
len [:omega,omega:] is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal set
X is set
T is set
a is V28() real ext-real set
a is V28() real ext-real set
].a,a.[ is V84() V85() V86() Element of bool REAL
A1 is V28() real ext-real rational set
T is Relation-like Function-like set
dom T is set
rng T is set
a is set
T . a is set
a is set
T . a is set
len X is epsilon-transitive epsilon-connected ordinal cardinal set
X is V84() V85() V86() Element of bool REAL
{ b1 where b1 is V28() real ext-real Element of REAL : (X,b1) } is set
a is set
a is V28() real ext-real Element of REAL
bool REAL is non empty non trivial non finite Element of bool (bool REAL)
A1 is V28() real ext-real set
].A1,a.[ is V84() V85() V86() Element of bool REAL
a is Relation-like Function-like set
dom a is set
rng a is set
a is set
A1 is set
a . a is set
a . A1 is set
a is V28() real ext-real set
B is V28() real ext-real set
].B,a.[ is V84() V85() V86() Element of bool REAL
C is V28() real ext-real Element of REAL
C is V28() real ext-real set
y is V28() real ext-real set
].y,C.[ is V84() V85() V86() Element of bool REAL
C is V28() real ext-real rational set
b is V28() real ext-real Element of REAL
len { b1 where b1 is V28() real ext-real Element of REAL : (X,b1) } is epsilon-transitive epsilon-connected ordinal cardinal set
len (rng a) is epsilon-transitive epsilon-connected ordinal cardinal set
a is set
A1 is set
A2 is set
a . A2 is set
a is V28() real ext-real set
a is V28() real ext-real set
].a,a.[ is V84() V85() V86() Element of bool REAL
B is V28() real ext-real Element of REAL
B is set
a . B is set
C is V28() real ext-real set
y is V28() real ext-real set
].y,C.[ is V84() V85() V86() Element of bool REAL
C is set
b is V28() real ext-real Element of REAL
c15 is V28() real ext-real Element of REAL
a is set
A1 is set
a . A1 is set
A2 is V28() real ext-real set
a is V28() real ext-real set
].a,A2.[ is V84() V85() V86() Element of bool REAL
B is V28() real ext-real set
a is V28() real ext-real set
].a,B.[ is V84() V85() V86() Element of bool REAL
X is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal set
exp (2,X) is epsilon-transitive epsilon-connected ordinal cardinal set
len X is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal set
bool X is non empty non trivial non finite Element of bool (bool X)
bool X is non empty non trivial non finite set
bool (bool X) is non empty non trivial non finite set
len (bool X) is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal set
len REAL is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal set
() is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal set
len { [.b1,b2.[ where b1, b2 is V28() real ext-real Element of REAL : ( not b2 <= b1 & b2 is rational ) } is epsilon-transitive epsilon-connected ordinal cardinal set
[:REAL,RAT:] is non empty non trivial RAT -valued V37() V38() V39() non finite set
T is Relation-like Function-like set
dom T is set
rng T is set
a is set
a is V28() real ext-real Element of REAL
A1 is V28() real ext-real Element of REAL
[.a,A1.[ is V84() V85() V86() Element of bool REAL
[a,A1] is Element of [:REAL,REAL:]
[:REAL,REAL:] is non empty non trivial V37() V38() V39() non finite set
{a,A1} is non empty finite V84() V85() V86() set
{a} is non empty trivial finite 1 -element V84() V85() V86() set
{{a,A1},{a}} is non empty finite V51() set
A2 is Element of [:REAL,RAT:]
A2 `2 is V28() real ext-real rational Element of RAT
A2 `1 is V28() real ext-real Element of REAL
T . A2 is set
len [:REAL,RAT:] is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal set
[:(len REAL),(len RAT):] is non empty non trivial non finite set
len [:(len REAL),(len RAT):] is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal set
() *` omega is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal set
a is set
a is V28() real ext-real Element of REAL
a + 1 is V28() real ext-real set
a + 0 is V28() real ext-real set
A1 is V28() real ext-real rational set
A2 is V28() real ext-real Element of REAL
[.a,A2.[ is V84() V85() V86() Element of bool REAL
a is Relation-like Function-like set
dom a is set
rng a is set
a is set
a . a is set
A1 is set
a . A1 is set
A2 is V28() real ext-real Element of REAL
a is V28() real ext-real Element of REAL
[.A2,a.[ is V84() V85() V86() Element of bool REAL
a is V28() real ext-real Element of REAL
B is V28() real ext-real Element of REAL
[.a,B.[ is V84() V85() V86() Element of bool REAL
X is set
T is V28() real ext-real set
a is set
In (a,NAT) is epsilon-transitive epsilon-connected ordinal natural V28() real ext-real finite cardinal integer rational V84() V85() V86() V87() V88() V89() Element of NAT
T |^ (In (a,NAT)) is V28() real ext-real set
a is non empty Relation-like NAT -defined REAL -valued Function-like V33( NAT ) V34( NAT , REAL ) V37() V38() V39() Element of bool [:NAT,REAL:]
a is epsilon-transitive epsilon-connected ordinal natural V28() real ext-real finite cardinal integer rational set
a . a is V28() real ext-real Element of REAL
T |^ a is V28() real ext-real set
In (a,NAT) is epsilon-transitive epsilon-connected ordinal natural V28() real ext-real finite cardinal integer rational V84() V85() V86() V87() V88() V89() Element of NAT
a is non empty Relation-like NAT -defined REAL -valued Function-like V33( NAT ) V34( NAT , REAL ) V37() V38() V39() Element of bool [:NAT,REAL:]
a is non empty Relation-like NAT -defined REAL -valued Function-like V33( NAT ) V34( NAT , REAL ) V37() V38() V39() Element of bool [:NAT,REAL:]
A1 is epsilon-transitive epsilon-connected ordinal natural V28() real ext-real finite cardinal integer rational V84() V85() V86() V87() V88() V89() Element of NAT
a . A1 is V28() real ext-real Element of REAL
T |^ A1 is V28() real ext-real set
a . A1 is V28() real ext-real Element of REAL
X is set
T is V28() real ext-real set
(X,T) is non empty Relation-like NAT -defined REAL -valued Function-like V33( NAT ) V34( NAT , REAL ) V37() V38() V39() Element of bool [:NAT,REAL:]
a is epsilon-transitive epsilon-connected ordinal natural V28() real ext-real finite cardinal integer rational V84() V85() V86() V87() V88() V89() Element of NAT
(X,T) . a is V28() real ext-real Element of REAL
T |^ a is V28() real ext-real set
a is non empty epsilon-transitive epsilon-connected ordinal natural V28() real ext-real positive finite cardinal integer rational V84() V85() V86() V87() V88() V89() Element of NAT
a is epsilon-transitive epsilon-connected ordinal natural V28() real ext-real finite cardinal integer rational V84() V85() V86() V87() V88() V89() Element of NAT
T GeoSeq is non empty Relation-like NAT -defined REAL -valued Function-like V33( NAT ) V34( NAT , REAL ) V37() V38() V39() Element of bool [:NAT,REAL:]
(T GeoSeq) . a is V28() real ext-real Element of REAL
T |^ a is V28() real ext-real set
(X,T) . a is V28() real ext-real Element of REAL
abs T is V28() real ext-real Element of REAL
a is non empty epsilon-transitive epsilon-connected ordinal natural V28() real ext-real positive finite cardinal integer rational V84() V85() V86() V87() V88() V89() Element of NAT
X is V28() real ext-real set
X GeoSeq is non empty Relation-like NAT -defined REAL -valued Function-like V33( NAT ) V34( NAT , REAL ) V37() V38() V39() Element of bool [:NAT,REAL:]
1 - X is V28() real ext-real set
T is epsilon-transitive epsilon-connected ordinal natural V28() real ext-real finite cardinal integer rational V84() V85() V86() V87() V88() V89() Element of NAT
(X GeoSeq) ^\ T is non empty Relation-like NAT -defined REAL -valued Function-like V33( NAT ) V34( NAT , REAL ) V37() V38() V39() Element of bool [:NAT,REAL:]
Sum ((X GeoSeq) ^\ T) is V28() real ext-real Element of REAL
X |^ T is V28() real ext-real set
(X |^ T) / (1 - X) is V28() real ext-real Element of COMPLEX
abs X is V28() real ext-real Element of REAL
(X |^ T) (#) (X GeoSeq) is non empty Relation-like NAT -defined REAL -valued Function-like V33( NAT ) V34( NAT , REAL ) V37() V38() V39() Element of bool [:NAT,REAL:]
dom ((X |^ T) (#) (X GeoSeq)) is V84() V85() V86() V87() V88() V89() Element of bool NAT
a is epsilon-transitive epsilon-connected ordinal natural V28() real ext-real finite cardinal integer rational V84() V85() V86() V87() V88() V89() Element of NAT
((X GeoSeq) ^\ T) . a is V28() real ext-real Element of REAL
a + T is epsilon-transitive epsilon-connected ordinal natural V28() real ext-real finite cardinal integer rational V84() V85() V86() V87() V88() V89() Element of NAT
(X GeoSeq) . (a + T) is V28() real ext-real Element of REAL
X |^ (a + T) is V28() real ext-real set
X |^ a is V28() real ext-real set
(X |^ T) * (X |^ a) is V28() real ext-real set
(X GeoSeq) . a is V28() real ext-real Element of REAL
(X |^ T) * ((X GeoSeq) . a) is V28() real ext-real set
((X |^ T) (#) (X GeoSeq)) . a is V28() real ext-real Element of REAL
Sum (X GeoSeq) is V28() real ext-real Element of REAL
1 / (1 - X) is V28() real ext-real Element of COMPLEX
(X |^ T) * (1 / (1 - X)) is V28() real ext-real set
(X |^ T) * 1 is V28() real ext-real set
((X |^ T) * 1) / (1 - X) is V28() real ext-real Element of COMPLEX
1 / 2 is V28() real ext-real rational Element of COMPLEX
(1 / 2) GeoSeq is non empty Relation-like NAT -defined REAL -valued Function-like V33( NAT ) V34( NAT , REAL ) V37() V38() V39() Element of bool [:NAT,REAL:]
X is epsilon-transitive epsilon-connected ordinal natural V28() real ext-real finite cardinal integer rational V84() V85() V86() V87() V88() V89() Element of NAT
X + 1 is epsilon-transitive epsilon-connected ordinal natural V28() real ext-real finite cardinal integer rational V84() V85() V86() V87() V88() V89() Element of NAT
((1 / 2) GeoSeq) ^\ (X + 1) is non empty Relation-like NAT -defined REAL -valued Function-like V33( NAT ) V34( NAT , REAL ) V37() V38() V39() Element of bool [:NAT,REAL:]
Sum (((1 / 2) GeoSeq) ^\ (X + 1)) is V28() real ext-real Element of REAL
(1 / 2) |^ X is V28() real ext-real set
(1 / 2) |^ (X + 1) is V28() real ext-real set
1 - (1 / 2) is V28() real ext-real rational set
((1 / 2) |^ (X + 1)) / (1 - (1 / 2)) is V28() real ext-real Element of COMPLEX
((1 / 2) |^ X) * (1 / 2) is V28() real ext-real set
(((1 / 2) |^ X) * (1 / 2)) / (1 / 2) is V28() real ext-real Element of COMPLEX
X is V28() real ext-real set
X GeoSeq is non empty Relation-like NAT -defined REAL -valued Function-like V33( NAT ) V34( NAT , REAL ) V37() V38() V39() Element of bool [:NAT,REAL:]
Sum (X GeoSeq) is V28() real ext-real Element of REAL
T is set
(T,X) is non empty Relation-like NAT -defined REAL -valued Function-like V33( NAT ) V34( NAT , REAL ) V37() V38() V39() Element of bool [:NAT,REAL:]
Sum (T,X) is V28() real ext-real Element of REAL
a is epsilon-transitive epsilon-connected ordinal natural V28() real ext-real finite cardinal integer rational V84() V85() V86() V87() V88() V89() Element of NAT
(T,X) . a is V28() real ext-real Element of REAL
X |^ a is V28() real ext-real set
(X GeoSeq) . a is V28() real ext-real Element of REAL
abs X is V28() real ext-real Element of REAL
X is set
(X,(1 / 2)) is non empty Relation-like NAT -defined REAL -valued Function-like V33( NAT ) V34( NAT , REAL ) V37() V38() V39() Element of bool [:NAT,REAL:]
T is epsilon-transitive epsilon-connected ordinal natural V28() real ext-real finite cardinal integer rational V84() V85() V86() V87() V88() V89() Element of NAT
T + 1 is epsilon-transitive epsilon-connected ordinal natural V28() real ext-real finite cardinal integer rational V84() V85() V86() V87() V88() V89() Element of NAT
(X,(1 / 2)) ^\ (T + 1) is non empty Relation-like NAT -defined REAL -valued Function-like V33( NAT ) V34( NAT , REAL ) V37() V38() V39() Element of bool [:NAT,REAL:]
Sum ((X,(1 / 2)) ^\ (T + 1)) is V28() real ext-real Element of REAL
(1 / 2) |^ T is V28() real ext-real set
abs (1 / 2) is V28() real ext-real rational Element of REAL
((1 / 2) GeoSeq) ^\ (T + 1) is non empty Relation-like NAT -defined REAL -valued Function-like V33( NAT ) V34( NAT , REAL ) V37() V38() V39() Element of bool [:NAT,REAL:]
a is epsilon-transitive epsilon-connected ordinal natural V28() real ext-real finite cardinal integer rational V84() V85() V86() V87() V88() V89() Element of NAT
((X,(1 / 2)) ^\ (T + 1)) . a is V28() real ext-real Element of REAL
a + (T + 1) is epsilon-transitive epsilon-connected ordinal natural V28() real ext-real finite cardinal integer rational V84() V85() V86() V87() V88() V89() Element of NAT
(X,(1 / 2)) . (a + (T + 1)) is V28() real ext-real Element of REAL
(1 / 2) |^ (a + (T + 1)) is V28() real ext-real set
((1 / 2) GeoSeq) . (a + (T + 1)) is V28() real ext-real Element of REAL
(((1 / 2) GeoSeq) ^\ (T + 1)) . a is V28() real ext-real Element of REAL
Sum (((1 / 2) GeoSeq) ^\ (T + 1)) is V28() real ext-real Element of REAL
T is non empty non trivial non finite V84() V85() V86() V87() V88() V89() Element of bool NAT
(T,(1 / 2)) is non empty Relation-like NAT -defined REAL -valued Function-like V33( NAT ) V34( NAT , REAL ) V37() V38() V39() Element of bool [:NAT,REAL:]
Sum (T,(1 / 2)) is V28() real ext-real Element of REAL
Partial_Sums (T,(1 / 2)) is non empty Relation-like NAT -defined REAL -valued Function-like V33( NAT ) V34( NAT , REAL ) V37() V38() V39() Element of bool [:NAT,REAL:]
a is epsilon-transitive epsilon-connected ordinal natural V28() real ext-real finite cardinal integer rational set
(Partial_Sums (T,(1 / 2))) . a is V28() real ext-real Element of REAL
a + 1 is epsilon-transitive epsilon-connected ordinal natural V28() real ext-real finite cardinal integer rational V84() V85() V86() V87() V88() V89() Element of NAT
a is set
A1 is epsilon-transitive epsilon-connected ordinal natural V28() real ext-real finite cardinal integer rational V84() V85() V86() V87() V88() V89() Element of NAT
(T,(1 / 2)) . A1 is V28() real ext-real Element of REAL
(1 / 2) |^ A1 is V28() real ext-real set
a is epsilon-transitive epsilon-connected ordinal natural V28() real ext-real finite cardinal integer rational V84() V85() V86() V87() V88() V89() Element of NAT
(T,(1 / 2)) . a is V28() real ext-real Element of REAL
(1 / 2) |^ a is V28() real ext-real set
a is epsilon-transitive epsilon-connected ordinal natural V28() real ext-real finite cardinal integer rational V84() V85() V86() V87() V88() V89() Element of NAT
a + a is epsilon-transitive epsilon-connected ordinal natural V28() real ext-real finite cardinal integer rational V84() V85() V86() V87() V88() V89() Element of NAT
(Partial_Sums (T,(1 / 2))) . (a + a) is V28() real ext-real Element of REAL
a + 1 is epsilon-transitive epsilon-connected ordinal natural V28() real ext-real finite cardinal integer rational V84() V85() V86() V87() V88() V89() Element of NAT
a + (a + 1) is epsilon-transitive epsilon-connected ordinal natural V28() real ext-real finite cardinal integer rational V84() V85() V86() V87() V88() V89() Element of NAT
(a + a) + 1 is epsilon-transitive epsilon-connected ordinal natural V28() real ext-real finite cardinal integer rational V84() V85() V86() V87() V88() V89() Element of NAT
A2 is epsilon-transitive epsilon-connected ordinal natural V28() real ext-real finite cardinal integer rational V84() V85() V86() V87() V88() V89() Element of NAT
A2 + (a + 1) is epsilon-transitive epsilon-connected ordinal natural V28() real ext-real finite cardinal integer rational V84() V85() V86() V87() V88() V89() Element of NAT
(Partial_Sums (T,(1 / 2))) . (A2 + (a + 1)) is V28() real ext-real Element of REAL
A2 + a is epsilon-transitive epsilon-connected ordinal natural V28() real ext-real finite cardinal integer rational V84() V85() V86() V87() V88() V89() Element of NAT
(Partial_Sums (T,(1 / 2))) . (A2 + a) is V28() real ext-real Element of REAL
(T,(1 / 2)) . (A2 + (a + 1)) is V28() real ext-real Element of REAL
((Partial_Sums (T,(1 / 2))) . (A2 + a)) + ((T,(1 / 2)) . (A2 + (a + 1))) is V28() real ext-real set
((Partial_Sums (T,(1 / 2))) . (A2 + a)) + 0 is V28() real ext-real set
(Partial_Sums (T,(1 / 2))) . (a + (a + 1)) is V28() real ext-real Element of REAL
A2 + 1 is epsilon-transitive epsilon-connected ordinal natural V28() real ext-real finite cardinal integer rational V84() V85() V86() V87() V88() V89() Element of NAT
a is epsilon-transitive epsilon-connected ordinal natural V28() real ext-real finite cardinal integer rational set
(A2 + 1) + a is epsilon-transitive epsilon-connected ordinal natural V28() real ext-real finite cardinal integer rational V84() V85() V86() V87() V88() V89() Element of NAT
((Partial_Sums (T,(1 / 2))) . a) + ((1 / 2) |^ A1) is V28() real ext-real set
((Partial_Sums (T,(1 / 2))) . a) + 0 is V28() real ext-real set
a + 0 is epsilon-transitive epsilon-connected ordinal natural V28() real ext-real finite cardinal integer rational V84() V85() V86() V87() V88() V89() Element of NAT
(Partial_Sums (T,(1 / 2))) . (a + 0) is V28() real ext-real Element of REAL
a is epsilon-transitive epsilon-connected ordinal natural V28() real ext-real finite cardinal integer rational V84() V85() V86() V87() V88() V89() Element of NAT
a + a is epsilon-transitive epsilon-connected ordinal natural V28() real ext-real finite cardinal integer rational V84() V85() V86() V87() V88() V89() Element of NAT
(Partial_Sums (T,(1 / 2))) . (a + a) is V28() real ext-real Element of REAL
a + 1 is epsilon-transitive epsilon-connected ordinal natural V28() real ext-real finite cardinal integer rational V84() V85() V86() V87() V88() V89() Element of NAT
A2 + (a + 1) is epsilon-transitive epsilon-connected ordinal natural V28() real ext-real finite cardinal integer rational V84() V85() V86() V87() V88() V89() Element of NAT
A2 + a is epsilon-transitive epsilon-connected ordinal natural V28() real ext-real finite cardinal integer rational V84() V85() V86() V87() V88() V89() Element of NAT
(A2 + a) + 1 is epsilon-transitive epsilon-connected ordinal natural V28() real ext-real finite cardinal integer rational V84() V85() V86() V87() V88() V89() Element of NAT
(Partial_Sums (T,(1 / 2))) . A1 is V28() real ext-real Element of REAL
(Partial_Sums (T,(1 / 2))) . (A2 + a) is V28() real ext-real Element of REAL
((Partial_Sums (T,(1 / 2))) . (A2 + a)) + ((1 / 2) |^ A1) is V28() real ext-real set
T is non empty non trivial non finite V84() V85() V86() V87() V88() V89() Element of bool NAT
(T,(1 / 2)) is non empty Relation-like NAT -defined REAL -valued Function-like V33( NAT ) V34( NAT , REAL ) V37() V38() V39() Element of bool [:NAT,REAL:]
Sum (T,(1 / 2)) is V28() real ext-real Element of REAL
a is non empty non trivial non finite V84() V85() V86() V87() V88() V89() Element of bool NAT
(a,(1 / 2)) is non empty Relation-like NAT -defined REAL -valued Function-like V33( NAT ) V34( NAT , REAL ) V37() V38() V39() Element of bool [:NAT,REAL:]
Sum (a,(1 / 2)) is V28() real ext-real Element of REAL
a is set
A1 is set
a is epsilon-transitive epsilon-connected ordinal natural V28() real ext-real finite cardinal integer rational set
A1 is epsilon-transitive epsilon-connected ordinal natural V28() real ext-real finite cardinal integer rational V84() V85() V86() V87() V88() V89() Element of NAT
A2 is non empty non trivial non finite V84() V85() V86() V87() V88() V89() Element of bool NAT
a is non empty non trivial non finite V84() V85() V86() V87() V88() V89() Element of bool NAT
(A2,(1 / 2)) is non empty Relation-like NAT -defined REAL -valued Function-like V33( NAT ) V34( NAT , REAL ) V37() V38() V39() Element of bool [:NAT,REAL:]
(A2,(1 / 2)) . A1 is V28() real ext-real Element of REAL
(1 / 2) |^ A1 is V28() real ext-real set
Partial_Sums (A2,(1 / 2)) is non empty Relation-like NAT -defined REAL -valued Function-like V33( NAT ) V34( NAT , REAL ) V37() V38() V39() Element of bool [:NAT,REAL:]
(a,(1 / 2)) is non empty Relation-like NAT -defined REAL -valued Function-like V33( NAT ) V34( NAT , REAL ) V37() V38() V39() Element of bool [:NAT,REAL:]
Partial_Sums (a,(1 / 2)) is non empty Relation-like NAT -defined REAL -valued Function-like V33( NAT ) V34( NAT , REAL ) V37() V38() V39() Element of bool [:NAT,REAL:]
a is epsilon-transitive epsilon-connected ordinal natural V28() real ext-real finite cardinal integer rational V84() V85() V86() V87() V88() V89() Element of NAT
(Partial_Sums (A2,(1 / 2))) . a is V28() real ext-real Element of REAL
(Partial_Sums (a,(1 / 2))) . a is V28() real ext-real Element of REAL
a + 1 is epsilon-transitive epsilon-connected ordinal natural V28() real ext-real finite cardinal integer rational V84() V85() V86() V87() V88() V89() Element of NAT
(Partial_Sums (A2,(1 / 2))) . (a + 1) is V28() real ext-real Element of REAL
(Partial_Sums (a,(1 / 2))) . (a + 1) is V28() real ext-real Element of REAL
(a,(1 / 2)) . (a + 1) is V28() real ext-real Element of REAL
(1 / 2) |^ (a + 1) is V28() real ext-real set
(A2,(1 / 2)) . (a + 1) is V28() real ext-real Element of REAL
((Partial_Sums (a,(1 / 2))) . a) + ((A2,(1 / 2)) . (a + 1)) is V28() real ext-real set
(Partial_Sums (A2,(1 / 2))) . 0 is V28() real ext-real Element of REAL
(A2,(1 / 2)) . 0 is V28() real ext-real Element of REAL
(1 / 2) |^ 0 is V28() real ext-real set
(a,(1 / 2)) . A1 is V28() real ext-real Element of REAL
(Partial_Sums (a,(1 / 2))) . 0 is V28() real ext-real Element of REAL
(a,(1 / 2)) . 0 is V28() real ext-real Element of REAL
(Partial_Sums (A2,(1 / 2))) . A1 is V28() real ext-real Element of REAL
(Partial_Sums (a,(1 / 2))) . A1 is V28() real ext-real Element of REAL
((Partial_Sums (a,(1 / 2))) . A1) + ((1 / 2) |^ A1) is V28() real ext-real set
a is epsilon-transitive epsilon-connected ordinal natural V28() real ext-real finite cardinal integer rational set
a + 1 is epsilon-transitive epsilon-connected ordinal natural V28() real ext-real finite cardinal integer rational V84() V85() V86() V87() V88() V89() Element of NAT
a is epsilon-transitive epsilon-connected ordinal natural V28() real ext-real finite cardinal integer rational set
a + 1 is epsilon-transitive epsilon-connected ordinal natural V28() real ext-real finite cardinal integer rational V84() V85() V86() V87() V88() V89() Element of NAT
B is epsilon-transitive epsilon-connected ordinal natural V28() real ext-real finite cardinal integer rational V84() V85() V86() V87() V88() V89() Element of NAT
(Partial_Sums (A2,(1 / 2))) . B is V28() real ext-real Element of REAL
(Partial_Sums (a,(1 / 2))) . B is V28() real ext-real Element of REAL
((Partial_Sums (a,(1 / 2))) . B) + 0 is V28() real ext-real set
(((Partial_Sums (a,(1 / 2))) . B) + 0) + ((1 / 2) |^ A1) is V28() real ext-real set
Sum (A2,(1 / 2)) is V28() real ext-real Element of REAL
A1 + 1 is epsilon-transitive epsilon-connected ordinal natural V28() real ext-real finite cardinal integer rational V84() V85() V86() V87() V88() V89() Element of NAT
(a,(1 / 2)) ^\ (A1 + 1) is non empty Relation-like NAT -defined REAL -valued Function-like V33( NAT ) V34( NAT , REAL ) V37() V38() V39() Element of bool [:NAT,REAL:]
Sum ((a,(1 / 2)) ^\ (A1 + 1)) is V28() real ext-real Element of REAL
Sum (a,(1 / 2)) is V28() real ext-real Element of REAL
((Partial_Sums (a,(1 / 2))) . A1) + (Sum ((a,(1 / 2)) ^\ (A1 + 1))) is V28() real ext-real set
X is set
Fin X is preBoolean set
{{}} is non empty trivial finite V51() 1 -element V84() V85() V86() V87() V88() V89() set
X * is set
T is set
a is Relation-like Function-like FinSequence-like set
rng a is set
T is Relation-like Function-like set
dom T is set
rng T is set
a is set
T . a is set
a is set
T . a is set
A1 is Relation-like Function-like FinSequence-like set
rng A1 is set
A2 is Relation-like Function-like FinSequence-like set
rng A2 is set
len (Fin X) is epsilon-transitive epsilon-connected ordinal cardinal set
len (X *) is epsilon-transitive epsilon-connected ordinal cardinal set
exp (2,omega) is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal set
[0,0] is Element of [:NAT,NAT:]
[:NAT,NAT:] is non empty non trivial RAT -valued INT -valued V37() V38() V39() V40() non finite set
{0,0} is non empty finite V51() V84() V85() V86() V87() V88() V89() set
{0} is non empty trivial finite V51() 1 -element V84() V85() V86() V87() V88() V89() set
{{0,0},{0}} is non empty finite V51() set
{0} is non empty trivial proper finite V51() 1 -element V84() V85() V86() V87() V88() V89() Element of bool NAT
[:{0},RAT+:] is set
{[0,0]} is non empty trivial proper Relation-like NAT -defined NAT -valued INT -valued V37() V38() V39() V40() finite 1 -element Element of bool [:NAT,NAT:]
bool [:NAT,NAT:] is non empty non trivial non finite set
[:{0},RAT+:] \ {[0,0]} is Relation-like {0} -defined RAT+ -valued Element of bool [:{0},RAT+:]
bool [:{0},RAT+:] is non empty set
RAT+ \/ ([:{0},RAT+:] \ {[0,0]}) is set
bool RAT+ is non empty Element of bool (bool RAT+)
bool RAT is non empty non trivial non finite Element of bool (bool RAT)
bool RAT is non empty non trivial non finite set
bool (bool RAT) is non empty non trivial non finite set
RAT \/ (bool RAT) is non empty set
len REAL+ is epsilon-transitive epsilon-connected ordinal cardinal set
len (RAT \/ (bool RAT)) is non empty epsilon-transitive epsilon-connected ordinal cardinal set
bool NAT is non empty non trivial non finite Element of bool (bool NAT)
bool (bool NAT) is non empty non trivial non finite set
Fin NAT is preBoolean set
(bool NAT) \ (Fin NAT) is Element of bool (bool NAT)
len (bool RAT) is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal set
(len RAT) +` (len (bool RAT)) is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal set
(len REAL+) +` (len REAL+) is epsilon-transitive epsilon-connected ordinal cardinal set
(exp (2,omega)) +` (exp (2,omega)) is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal set
[:{0},REAL+:] is set
len [:{0},REAL+:] is epsilon-transitive epsilon-connected ordinal cardinal set
[:REAL+,{0}:] is RAT -valued INT -valued V37() V38() V39() V40() set
len [:REAL+,{0}:] is epsilon-transitive epsilon-connected ordinal cardinal set
REAL+ \/ [:{0},REAL+:] is set
len (REAL+ \/ [:{0},REAL+:]) is epsilon-transitive epsilon-connected ordinal cardinal set
(len REAL+) +` (len [:{0},REAL+:]) is epsilon-transitive epsilon-connected ordinal cardinal set
len (Fin NAT) is epsilon-transitive epsilon-connected ordinal cardinal set
len (bool NAT) is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal set
(len (bool NAT)) +` (len (Fin NAT)) is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal set
T is non empty set
[:T,REAL:] is non empty non trivial V37() V38() V39() non finite set
bool [:T,REAL:] is non empty non trivial non finite set
a is non empty Relation-like T -defined REAL -valued Function-like V33(T) V34(T, REAL ) V37() V38() V39() Element of bool [:T,REAL:]
a is set
dom a is set
a . a is V28() real ext-real set
A1 is set
a . A1 is V28() real ext-real set
dom a is Element of bool T
bool T is non empty set
(A1,(1 / 2)) is non empty Relation-like NAT -defined REAL -valued Function-like V33( NAT ) V34( NAT , REAL ) V37() V38() V39() Element of bool [:NAT,REAL:]
Sum (A1,(1 / 2)) is V28() real ext-real Element of REAL
(a,(1 / 2)) is non empty Relation-like NAT -defined REAL -valued Function-like V33( NAT ) V34( NAT , REAL ) V37() V38() V39() Element of bool [:NAT,REAL:]
Sum (a,(1 / 2)) is V28() real ext-real Element of REAL
rng a is V84() V85() V86() set
dom a is Element of bool T
bool T is non empty set
len T is non empty epsilon-transitive epsilon-connected ordinal cardinal set
bool omega is non empty non trivial non finite Element of bool (bool omega)
bool (bool omega) is non empty non trivial non finite set
len (bool omega) is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal set
{ b1 where b1 is V28() real ext-real Element of REAL : (a1,b1) } is set
X is Element of bool (bool REAL)
len X is epsilon-transitive epsilon-connected ordinal cardinal set
UniCl X is Element of bool (bool REAL)
{ b1 where b1 is V28() real ext-real Element of REAL : ex b2 being set st
( b2 in UniCl X & (b2,b1) ) } is set
len { b1 where b1 is V28() real ext-real Element of REAL : ex b2 being set st
( b2 in UniCl X & (b2,b1) ) } is epsilon-transitive epsilon-connected ordinal cardinal set
(len X) *` omega is epsilon-transitive epsilon-connected ordinal cardinal set
len (len X) is epsilon-transitive epsilon-connected ordinal cardinal set
(len X) *` omega is epsilon-transitive epsilon-connected ordinal cardinal set
(len X) *` omega is epsilon-transitive epsilon-connected ordinal cardinal set
(len X) *` omega is epsilon-transitive epsilon-connected ordinal cardinal set
(len X) *` omega is epsilon-transitive epsilon-connected ordinal cardinal set
{ b1 where b1 is V28() real ext-real Element of REAL : ex b2 being set st
( b2 in X & (b2,b1) ) } is set
bool REAL is non empty non trivial non finite Element of bool (bool REAL)
a is set
{ b1 where b1 is V28() real ext-real Element of REAL : (a,b1) } is set
A1 is set
A2 is V28() real ext-real Element of REAL
[:X,(bool REAL):] is set
bool [:X,(bool REAL):] is non empty set
a is Relation-like X -defined bool REAL -valued Function-like V33(X) V34(X, bool REAL) Element of bool [:X,(bool REAL):]
A1 is set
A2 is V28() real ext-real Element of REAL
a is set
a is set
a is V84() V85() V86() Element of bool REAL
B is Element of bool (bool REAL)
union B is V84() V85() V86() Element of bool REAL
C is set
y is V28() real ext-real set
].y,A2.[ is V84() V85() V86() Element of bool REAL
C is V84() V85() V86() Element of bool REAL
b is set
Union a is set
rng a is set
union (rng a) is set
A1 is set
dom a is Element of bool X
bool X is non empty set
A2 is V28() real ext-real Element of REAL
a is set
a is set
a . a is set
{ b1 where b1 is V28() real ext-real Element of REAL : (a,b1) } is set
len (Union a) is epsilon-transitive epsilon-connected ordinal cardinal set
A1 is set
a . A1 is set
len (a . A1) is epsilon-transitive epsilon-connected ordinal cardinal set
A2 is V84() V85() V86() Element of bool REAL
{ b1 where b1 is V28() real ext-real Element of REAL : (A2,b1) } is set
dom a is Element of bool X
bool X is non empty set
X is Element of bool (bool REAL)
len X is epsilon-transitive epsilon-connected ordinal cardinal set
UniCl X is Element of bool (bool REAL)
{ b1 where b1 is V28() real ext-real Element of REAL : ex b2 being set st
( b2 in UniCl X & (b2,b1) ) } is set
REAL \ { b1 where b1 is V28() real ext-real Element of REAL : ex b2 being set st
( b2 in UniCl X & (b2,b1) ) } is V84() V85() V86() Element of bool REAL
the V28() real ext-real Element of REAL \ { b1 where b1 is V28() real ext-real Element of REAL : ex b2 being set st
( b2 in UniCl X & (b2,b1) ) } is V28() real ext-real Element of REAL \ { b1 where b1 is V28() real ext-real Element of REAL : ex b2 being set st
( b2 in UniCl X & (b2,b1) ) }
len { b1 where b1 is V28() real ext-real Element of REAL : ex b2 being set st
( b2 in UniCl X & (b2,b1) ) } is epsilon-transitive epsilon-connected ordinal cardinal set
a is V28() real ext-real Element of REAL
a + 1 is V28() real ext-real set
a + 0 is V28() real ext-real set
A1 is V28() real ext-real rational set
[.a,A1.[ is V84() V85() V86() Element of bool REAL
a - 1 is V28() real ext-real set
A2 is V28() real ext-real set
].A2,a.[ is V84() V85() V86() Element of bool REAL
a - 0 is V28() real ext-real set
a is set
a is V28() real ext-real Element of REAL
weight () is epsilon-transitive epsilon-connected ordinal cardinal set
X is open quasi_basis Element of bool (bool the carrier of ())
len X is epsilon-transitive epsilon-connected ordinal cardinal set
UniCl X is Element of bool (bool the carrier of ())
a is V28() real ext-real rational set
T is V28() real ext-real set
[.T,a.[ is V84() V85() V86() Element of bool REAL
X is set
T is set
a is set
T \/ a is set
bool X is non empty set
a is Element of bool X
A1 is Element of bool X
a \/ A1 is Element of bool X
bool X is non empty set
bool (bool X) is non empty set
T is Element of bool (bool X)
Intersect T is Element of bool X
{X} is non empty trivial finite 1 -element set
a is set
T is strict 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
T is strict TopSpace-like TopStruct
the carrier of T is set
bool the carrier of T is non empty set
a is strict TopSpace-like TopStruct
the carrier of a is set
bool the carrier of a is non empty set
a is set
X is set
(X) is strict TopSpace-like TopStruct
the carrier of (X) is set
bool the carrier of (X) is non empty set
T is Element of bool the carrier of (X)
T ` is Element of bool the carrier of (X)
the carrier of (X) \ T is set
(T `) ` is Element of bool the carrier of (X)
the carrier of (X) \ (T `) is set
[#] the carrier of (X) is non proper Element of bool the carrier of (X)
X is non empty non trivial non finite set
bool X is non empty non trivial non finite set
T is Element of bool X
T ` is Element of bool X
X \ T is set
T \/ (T `) is Element of bool X
[#] X is non empty non trivial non proper Element of bool X
X is non empty set
(X) is strict TopSpace-like TopStruct
X is non empty non trivial non finite set
(X) is non empty strict TopSpace-like TopStruct
the carrier of (X) is non empty set
bool the carrier of (X) is non empty set
T is non empty open Element of bool the carrier of (X)
a is non empty open Element of bool the carrier of (X)
a ` is closed Element of bool the carrier of (X)
the carrier of (X) \ a is set
T ` is closed Element of bool the carrier of (X)
the carrier of (X) \ T is set
[#] the carrier of (X) is non empty non proper Element of bool the carrier of (X)
(T `) ` is open Element of bool the carrier of (X)
the carrier of (X) \ (T `) is set
{} the carrier of (X) is empty proper epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V28() real ext-real finite V51() cardinal {} -element integer rational V84() V85() V86() V87() V88() V89() V90() open closed boundary nowhere_dense Element of bool the carrier of (X)
X is set
T is set
{T} is non empty trivial finite 1 -element set
{T} /\ X is finite set
bool X is non empty set
a is Element of bool X
a \/ ({T} /\ X) is set
IFEQ (a,{},a,(a \/ ({T} /\ X))) is set
{} \/ ({T} /\ X) is finite set
IFEQ ({},{},{},({} \/ ({T} /\ X))) is set
a is Element of bool X
a is Element of bool X
a \/ a is Element of bool X
(a \/ a) \/ ({T} /\ X) is set
IFEQ ((a \/ a),{},(a \/ a),((a \/ a) \/ ({T} /\ X))) is set
a \/ ({T} /\ X) is set
IFEQ (a,{},a,(a \/ ({T} /\ X))) is set
a \/ ({T} /\ X) is set
IFEQ (a,{},a,(a \/ ({T} /\ X))) is set
H1(a) \/ H1(a) is set
a is Element of bool X
a \/ ({T} /\ X) is set
IFEQ (a,{},a,(a \/ ({T} /\ X))) is set
H1(a) \/ ({T} /\ X) is set
IFEQ (H1(a),{},H1(a),(H1(a) \/ ({T} /\ X))) is set
(a \/ ({T} /\ X)) \/ ({T} /\ X) is set
a is strict TopSpace-like TopStruct
the carrier of a is set
bool the carrier of a is non empty set
a is Element of bool the carrier of a
Cl a is closed Element of bool the carrier of a
a \/ ({T} /\ X) is set
IFEQ (a,{},a,(a \/ ({T} /\ X))) is set
a is strict TopSpace-like TopStruct
the carrier of a is set
bool the carrier of a is non empty set
a is strict TopSpace-like TopStruct
the carrier of a is set
bool the carrier of a is non empty set
A1 is Element of bool the carrier of a
A2 is Element of bool the carrier of a
Cl A1 is closed Element of bool the carrier of a
A2 \/ ({T} /\ X) is set
IFEQ (A2,{},A2,(A2 \/ ({T} /\ X))) is set
Cl A2 is closed Element of bool the carrier of a
X is non empty set
T is set
(X,T) is strict TopSpace-like TopStruct
X is non empty set
T is Element of X
(X,T) is non empty strict TopSpace-like TopStruct
the carrier of (X,T) is non empty set
bool the carrier of (X,T) is non empty set
{T} is non empty trivial finite 1 -element Element of bool X
bool X is non empty set
a is non empty Element of bool the carrier of (X,T)
Cl a is closed Element of bool the carrier of (X,T)
a \/ {T} is non empty set
{T} /\ X is finite Element of bool X
a \/ ({T} /\ X) is non empty set
IFEQ (a,{},a,(a \/ ({T} /\ X))) is set
X is non empty set
T is Element of X
(X,T) is non empty strict TopSpace-like TopStruct
the carrier of (X,T) is non empty set
bool the carrier of (X,T) is non empty set
a is non empty Element of bool the carrier of (X,T)
Cl a is closed Element of bool the carrier of (X,T)
{T} is non empty trivial finite 1 -element Element of bool X
bool X is non empty set
a \/ {T} is non empty set
X is non empty set
T is Element of X
(X,T) is non empty strict TopSpace-like TopStruct
the carrier of (X,T) is non empty set
bool the carrier of (X,T) is non empty set
a is proper Element of bool the carrier of (X,T)
a ` is non empty Element of bool the carrier of (X,T)
the carrier of (X,T) \ a is set
T is set
X is set
a is set
{a} is non empty trivial finite 1 -element set
(X,T) is strict TopSpace-like TopStruct
the carrier of (X,T) is set
bool the carrier of (X,T) is non empty set
T is set
{T} is non empty trivial finite 1 -element set
X is set
a is set
{a} is non empty trivial finite 1 -element set
(X,T) is strict TopSpace-like TopStruct
the carrier of (X,T) is set
bool the carrier of (X,T) is non empty set
a is non empty set
bool a is non empty set
A1 is Element of bool a
A2 is proper Element of bool a
(a,T) is non empty strict TopSpace-like TopStruct
the carrier of (a,T) is non empty set
bool the carrier of (a,T) is non empty set
X is set
T is set
bool X is non empty set
a is Element of bool X
a /\ T is set
IFEQ (a,X,a,(a /\ T)) is set
a /\ T is Element of bool X
a is Element of bool X
a is Element of bool X
a /\ a is Element of bool X
(a /\ a) /\ T is set
IFEQ ((a /\ a),X,(a /\ a),((a /\ a) /\ T)) is set
a /\ T is set
IFEQ (a,X,a,(a /\ T)) is set
a /\ T is set
IFEQ (a,X,a,(a /\ T)) is set
H1(a) /\ H1(a) is set
a /\ X is Element of bool X
a /\ T is Element of bool X
X /\ H1(a) is set
a /\ T is Element of bool X
H1(a) /\ X is set
a /\ X is Element of bool X
a \/ (a /\ a) is Element of bool X
(a /\ a) /\ T is Element of bool X
T /\ T is set
((a /\ a) /\ T) /\ T is Element of bool X
a /\ T is Element of bool X
(a /\ T) /\ a is Element of bool X
((a /\ T) /\ a) /\ T is Element of bool X
a /\ T is Element of bool X
a is Element of bool X
a /\ T is set
IFEQ (a,X,a,(a /\ T)) is set
H1(a) /\ T is set
IFEQ (H1(a),X,H1(a),(H1(a) /\ T)) is set
a /\ T is Element of bool X
(a /\ T) /\ T is Element of bool X
T /\ T is set
X /\ T is set
IFEQ (X,X,X,(X /\ T)) is set
a is strict TopSpace-like TopStruct
the carrier of a is set
bool the carrier of a is non empty set
a is Element of bool the carrier of a
Int a is open Element of bool the carrier of a
a /\ T is Element of bool the carrier of a
IFEQ (a,X,a,(a /\ T)) is Element of bool the carrier of a
a is strict TopSpace-like TopStruct
the carrier of a is set
bool the carrier of a is non empty set
a is strict TopSpace-like TopStruct
the carrier of a is set
bool the carrier of a is non empty set
A1 is Element of bool the carrier of a
A2 is Element of bool the carrier of a
Int A1 is open Element of bool the carrier of a
A2 /\ T is Element of bool the carrier of a
IFEQ (A2,X,A2,(A2 /\ T)) is Element of bool the carrier of a
Int A2 is open Element of bool the carrier of a
X is non empty set
T is set
(X,T) is strict TopSpace-like TopStruct
X is non empty set
T is set
(X,T) is non empty strict TopSpace-like TopStruct
the carrier of (X,T) is non empty set
bool the carrier of (X,T) is non empty set
a is proper Element of bool the carrier of (X,T)
Int a is open Element of bool the carrier of (X,T)
a /\ T is Element of bool the carrier of (X,T)
IFEQ (a,X,a,(a /\ T)) is Element of bool the carrier of (X,T)
X is non empty set
T is set
(X,T) is non empty strict TopSpace-like TopStruct
the carrier of (X,T) is non empty set
bool the carrier of (X,T) is non empty set
a is proper Element of bool the carrier of (X,T)
Int a is open Element of bool the carrier of (X,T)
a /\ T is Element of bool the carrier of (X,T)
X is set
bool X is non empty set
{X} is non empty trivial finite 1 -element set
T is Element of bool X
(X,T) is strict TopSpace-like TopStruct
the topology of (X,T) is non empty Element of bool (bool the carrier of (X,T))
the carrier of (X,T) is set
bool the carrier of (X,T) is non empty set
bool (bool the carrier of (X,T)) is non empty set
bool T is non empty Element of bool (bool T)
bool T is non empty set
bool (bool T) is non empty set
{X} \/ (bool T) is non empty set
a is set
a is Element of bool the carrier of (X,T)
a is set
a is Element of bool the carrier of (X,T)
[#] (X,T) is non proper open closed dense Element of bool the carrier of (X,T)
X is set
ADTS X is TopStruct
(X,{}) is strict TopSpace-like TopStruct
the carrier of (X,{}) is set
cobool X is Element of bool (bool X)
bool X is non empty set
bool (bool X) is non empty set
{{},X} is non empty finite set
the topology of (X,{}) is non empty Element of bool (bool the carrier of (X,{}))
bool the carrier of (X,{}) is non empty set
bool (bool the carrier of (X,{})) is non empty set
a is set
a is Element of bool the carrier of (X,{})
{} (X,{}) is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V28() real ext-real finite V51() cardinal {} -element integer rational V84() V85() V86() V87() V88() V89() V90() open closed boundary nowhere_dense Element of bool the carrier of (X,{})
[#] (X,{}) is non proper open closed dense Element of bool the carrier of (X,{})
X is set
1TopSp X is TopStruct
bool X is non empty Element of bool (bool X)
bool X is non empty set
bool (bool X) is non empty set
[#] (bool X) is non empty non proper Element of bool (bool X)
bool (bool X) is non empty set
TopStruct(# X,([#] (bool X)) #) is strict TopStruct
(X,X) is strict TopSpace-like TopStruct
the carrier of (X,X) is set
the topology of (X,X) is non empty Element of bool (bool the carrier of (X,X))
bool the carrier of (X,X) is non empty set
bool (bool the carrier of (X,X)) is non empty set
{X} is non empty trivial finite 1 -element set
{X} \/ (bool X) is non empty set