REAL is non empty non trivial non finite complex-membered ext-real-membered real-membered V47() non bounded_below non bounded_above interval non empty-membered set
NAT is epsilon-transitive epsilon-connected ordinal non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V47() left_end bounded_below Element of bool REAL
bool REAL is non empty set
ExtREAL is non empty ext-real-membered interval set
[:NAT,ExtREAL:] is Relation-like non empty ext-real-valued set
bool [:NAT,ExtREAL:] is non empty set
bool ExtREAL is non empty set
omega is epsilon-transitive epsilon-connected ordinal non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V47() left_end bounded_below set
bool omega is non empty set
COMPLEX is non empty non trivial non finite complex-membered V47() non empty-membered set
RAT is non empty non trivial non finite complex-membered ext-real-membered real-membered rational-membered V47() non empty-membered set
INT is non empty non trivial non finite complex-membered ext-real-membered real-membered rational-membered integer-membered V47() non empty-membered set
bool NAT is non empty set
[:COMPLEX,COMPLEX:] is Relation-like non empty complex-valued set
bool [:COMPLEX,COMPLEX:] is non empty set
[:COMPLEX,REAL:] is Relation-like non empty complex-valued ext-real-valued real-valued set
bool [:COMPLEX,REAL:] is non empty set
[:[:COMPLEX,COMPLEX:],COMPLEX:] is Relation-like non empty complex-valued set
bool [:[:COMPLEX,COMPLEX:],COMPLEX:] is non empty set
[:REAL,REAL:] is Relation-like non empty complex-valued ext-real-valued real-valued set
bool [:REAL,REAL:] is non empty set
[:[:REAL,REAL:],REAL:] is Relation-like non empty complex-valued ext-real-valued real-valued set
bool [:[:REAL,REAL:],REAL:] is non empty set
[:RAT,RAT:] is Relation-like RAT -valued non empty complex-valued ext-real-valued real-valued set
bool [:RAT,RAT:] is non empty set
[:[:RAT,RAT:],RAT:] is Relation-like RAT -valued non empty complex-valued ext-real-valued real-valued set
bool [:[:RAT,RAT:],RAT:] is non empty set
[:INT,INT:] is Relation-like RAT -valued INT -valued non empty complex-valued ext-real-valued real-valued set
bool [:INT,INT:] is non empty set
[:[:INT,INT:],INT:] is Relation-like RAT -valued INT -valued non empty complex-valued ext-real-valued real-valued set
bool [:[:INT,INT:],INT:] is non empty set
[:NAT,NAT:] is Relation-like RAT -valued INT -valued non empty complex-valued ext-real-valued real-valued natural-valued set
[:[:NAT,NAT:],NAT:] is Relation-like RAT -valued INT -valued non empty complex-valued ext-real-valued real-valued natural-valued set
bool [:[:NAT,NAT:],NAT:] is non empty set
{} is Relation-like non-zero empty-yielding RAT -valued epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural empty complex real ext-real non positive non negative finite finite-yielding V37() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V47() complex-valued ext-real-valued real-valued natural-valued bounded_below bounded_above real-bounded interval integer set
the Relation-like non-zero empty-yielding RAT -valued epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural empty complex real ext-real non positive non negative finite finite-yielding V37() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V47() complex-valued ext-real-valued real-valued natural-valued bounded_below bounded_above real-bounded interval integer set is Relation-like non-zero empty-yielding RAT -valued epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural empty complex real ext-real non positive non negative finite finite-yielding V37() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V47() complex-valued ext-real-valued real-valued natural-valued bounded_below bounded_above real-bounded interval integer set
1 is epsilon-transitive epsilon-connected ordinal natural non empty complex real ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end bounded_below integer V90() Element of NAT
{{},1} is non empty finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end right_end bounded_below bounded_above real-bounded set
0. is Relation-like non-zero empty-yielding RAT -valued epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural empty complex real ext-real non positive non negative finite finite-yielding V37() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V47() complex-valued ext-real-valued real-valued natural-valued bounded_below bounded_above real-bounded interval integer Element of ExtREAL
0 is Relation-like non-zero empty-yielding RAT -valued epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural empty complex real ext-real non positive non negative finite finite-yielding V37() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V47() complex-valued ext-real-valued real-valued natural-valued bounded_below bounded_above real-bounded interval integer V90() Element of NAT
K72(REAL,REAL,NAT,NAT) is Relation-like REAL -defined REAL -valued RAT -valued INT -valued non empty complex-valued ext-real-valued real-valued natural-valued Element of bool [:REAL,REAL:]
K155(NAT) is V38() set
K155(K72(REAL,REAL,NAT,NAT)) is V38() set
+infty is non empty non real ext-real positive non negative set
-infty is non empty non real ext-real non positive negative set
2 is epsilon-transitive epsilon-connected ordinal natural non empty complex real ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end bounded_below integer V90() Element of NAT
[:NAT,REAL:] is Relation-like non empty complex-valued ext-real-valued real-valued set
bool [:NAT,REAL:] is non empty set
0 " is Relation-like non-zero empty-yielding RAT -valued epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural empty complex real ext-real non positive non negative finite finite-yielding V37() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V47() complex-valued ext-real-valued real-valued natural-valued bounded_below bounded_above real-bounded interval integer set
[:NAT,[:NAT,NAT:]:] is Relation-like non empty set
bool [:NAT,[:NAT,NAT:]:] is non empty set
A is Relation-like Function-like set
dom A is set
rng A is set
A is Relation-like NAT -defined ExtREAL -valued non empty Function-like total V30( NAT , ExtREAL ) ext-real-valued Element of bool [:NAT,ExtREAL:]
SUM A is ext-real Element of ExtREAL
Ser A is Relation-like NAT -defined ExtREAL -valued non empty Function-like total V30( NAT , ExtREAL ) ext-real-valued Element of bool [:NAT,ExtREAL:]
rng (Ser A) is non empty ext-real-membered V67() Element of bool ExtREAL
sup (rng (Ser A)) is ext-real Element of ExtREAL
(Ser A) . 0 is ext-real Element of ExtREAL
A is Relation-like NAT -defined ExtREAL -valued non empty Function-like total V30( NAT , ExtREAL ) ext-real-valued Element of bool [:NAT,ExtREAL:]
SUM A is ext-real Element of ExtREAL
Ser A is Relation-like NAT -defined ExtREAL -valued non empty Function-like total V30( NAT , ExtREAL ) ext-real-valued Element of bool [:NAT,ExtREAL:]
rng (Ser A) is non empty ext-real-membered V67() Element of bool ExtREAL
sup (rng (Ser A)) is ext-real Element of ExtREAL
x is ext-real Element of ExtREAL
a is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below integer V90() Element of NAT
A . a is ext-real Element of ExtREAL
a is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below integer V90() Element of NAT
A . a is ext-real Element of ExtREAL
(Ser A) . a is ext-real Element of ExtREAL
a is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer set
a + 1 is epsilon-transitive epsilon-connected ordinal natural non empty complex real ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end bounded_below integer V90() Element of NAT
a is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer set
a + 1 is epsilon-transitive epsilon-connected ordinal natural non empty complex real ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end bounded_below integer V90() Element of NAT
c5 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below integer V90() Element of NAT
(Ser A) . c5 is ext-real Element of ExtREAL
c5 + 1 is epsilon-transitive epsilon-connected ordinal natural non empty complex real ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end bounded_below integer V90() Element of NAT
A . (c5 + 1) is ext-real Element of ExtREAL
((Ser A) . c5) + (A . (c5 + 1)) is ext-real Element of ExtREAL
0. + x is ext-real Element of ExtREAL
A is ext-real set
A is ext-real Element of ExtREAL
x is complex real ext-real set
a is complex real ext-real set
a + a is complex real ext-real set
a + a is complex real ext-real set
c5 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below integer V90() Element of NAT
r3 is ext-real Element of ExtREAL
r3 / 2 is ext-real set
2 " is complex real ext-real non negative set
2 " is non empty complex real ext-real positive non negative set
r3 * (2 ") is ext-real set
x1 is ext-real Element of ExtREAL
m1 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below integer V90() Element of NAT
n is ext-real Element of ExtREAL
m is ext-real Element of ExtREAL
n / 2 is ext-real set
n * (2 ") is ext-real set
a is ext-real Element of ExtREAL
c5 is Relation-like NAT -defined ExtREAL -valued non empty Function-like total V30( NAT , ExtREAL ) ext-real-valued Element of bool [:NAT,ExtREAL:]
c5 . 0 is ext-real Element of ExtREAL
SUM c5 is ext-real Element of ExtREAL
Ser c5 is Relation-like NAT -defined ExtREAL -valued non empty Function-like total V30( NAT , ExtREAL ) ext-real-valued Element of bool [:NAT,ExtREAL:]
rng (Ser c5) is non empty ext-real-membered V67() Element of bool ExtREAL
sup (rng (Ser c5)) is ext-real Element of ExtREAL
r3 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below integer V90() Element of NAT
c5 . r3 is ext-real Element of ExtREAL
r3 + 1 is epsilon-transitive epsilon-connected ordinal natural non empty complex real ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end bounded_below integer V90() Element of NAT
c5 . (r3 + 1) is ext-real Element of ExtREAL
(c5 . r3) / 2 is ext-real set
2 " is complex real ext-real non negative set
2 " is non empty complex real ext-real positive non negative set
(c5 . r3) * (2 ") is ext-real set
r3 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below integer V90() Element of NAT
c5 . r3 is ext-real Element of ExtREAL
r3 is ext-real set
dom (Ser c5) is non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end bounded_below Element of bool NAT
x1 is set
(Ser c5) . x1 is ext-real Element of ExtREAL
m is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below integer V90() Element of NAT
(Ser c5) . m is ext-real Element of ExtREAL
c5 . m is ext-real Element of ExtREAL
((Ser c5) . m) + (c5 . m) is ext-real Element of ExtREAL
m + 1 is epsilon-transitive epsilon-connected ordinal natural non empty complex real ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end bounded_below integer V90() Element of NAT
(Ser c5) . (m + 1) is ext-real Element of ExtREAL
c5 . (m + 1) is ext-real Element of ExtREAL
((Ser c5) . (m + 1)) + (c5 . (m + 1)) is ext-real Element of ExtREAL
(c5 . m) / 2 is ext-real set
2 " is complex real ext-real non negative set
2 " is non empty complex real ext-real positive non negative set
(c5 . m) * (2 ") is ext-real set
(c5 . (m + 1)) + (c5 . (m + 1)) is ext-real Element of ExtREAL
((Ser c5) . m) + ((c5 . (m + 1)) + (c5 . (m + 1))) is ext-real Element of ExtREAL
((Ser c5) . m) + (c5 . (m + 1)) is ext-real Element of ExtREAL
(((Ser c5) . m) + (c5 . (m + 1))) + (c5 . (m + 1)) is ext-real Element of ExtREAL
(Ser c5) . 0 is ext-real Element of ExtREAL
((Ser c5) . 0) + (c5 . 0) is ext-real Element of ExtREAL
n is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below integer V90() Element of NAT
(Ser c5) . n is ext-real Element of ExtREAL
c5 . n is ext-real Element of ExtREAL
((Ser c5) . n) + (c5 . n) is ext-real Element of ExtREAL
A is ext-real Element of ExtREAL
x is non empty ext-real-membered Element of bool ExtREAL
inf x is ext-real Element of ExtREAL
(inf x) + A is ext-real Element of ExtREAL
+infty is non empty non real ext-real positive non negative Element of ExtREAL
a is complex real ext-real Element of REAL
a is complex real ext-real Element of REAL
a + a is complex real ext-real Element of REAL
a - a is complex real ext-real Element of REAL
- a is complex real ext-real set
a + (- a) is complex real ext-real set
+infty is non empty non real ext-real positive non negative Element of ExtREAL
+infty is non empty non real ext-real positive non negative Element of ExtREAL
A is ext-real Element of ExtREAL
x is non empty ext-real-membered Element of bool ExtREAL
sup x is ext-real Element of ExtREAL
(sup x) - A is ext-real Element of ExtREAL
- A is ext-real set
(sup x) + (- A) is ext-real set
+infty is non empty non real ext-real positive non negative Element of ExtREAL
a is complex real ext-real Element of REAL
a is complex real ext-real Element of REAL
a - a is complex real ext-real Element of REAL
- a is complex real ext-real set
a + (- a) is complex real ext-real set
+infty is non empty non real ext-real positive non negative Element of ExtREAL
-infty is non empty non real ext-real non positive negative Element of ExtREAL
+infty is non empty non real ext-real positive non negative Element of ExtREAL
+infty is non empty non real ext-real positive non negative Element of ExtREAL
A is Relation-like NAT -defined ExtREAL -valued non empty Function-like total V30( NAT , ExtREAL ) ext-real-valued Element of bool [:NAT,ExtREAL:]
SUM A is ext-real Element of ExtREAL
Ser A is Relation-like NAT -defined ExtREAL -valued non empty Function-like total V30( NAT , ExtREAL ) ext-real-valued Element of bool [:NAT,ExtREAL:]
rng (Ser A) is non empty ext-real-membered V67() Element of bool ExtREAL
sup (rng (Ser A)) is ext-real Element of ExtREAL
x is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below integer V90() Element of NAT
A . x is ext-real Element of ExtREAL
a is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below integer V90() Element of NAT
A . a is ext-real Element of ExtREAL
(Ser A) . a is ext-real Element of ExtREAL
a + 1 is epsilon-transitive epsilon-connected ordinal natural non empty complex real ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end bounded_below integer V90() Element of NAT
A . (a + 1) is ext-real Element of ExtREAL
(Ser A) . (a + 1) is ext-real Element of ExtREAL
a is ext-real Element of ExtREAL
a + (A . (a + 1)) is ext-real Element of ExtREAL
A . 0 is ext-real Element of ExtREAL
(Ser A) . 0 is ext-real Element of ExtREAL
(Ser A) . x is ext-real Element of ExtREAL
[#] REAL is non empty non proper complex-membered ext-real-membered real-membered closed open Element of bool REAL
x is ext-real Element of ExtREAL
a is ext-real Element of ExtREAL
A is non empty complex-membered ext-real-membered real-membered interval Element of bool REAL
].x,a.[ is complex-membered ext-real-membered real-membered non left_end non right_end interval Element of bool REAL
{ b1 where b1 is complex real ext-real Element of REAL : ( not b1 <= x & not a <= b1 ) } is set
inf A is ext-real Element of ExtREAL
x is ext-real Element of ExtREAL
a is ext-real Element of ExtREAL
A is non empty complex-membered ext-real-membered real-membered interval Element of bool REAL
].x,a.] is ext-real-membered non left_end interval set
inf A is ext-real Element of ExtREAL
x is ext-real Element of ExtREAL
a is ext-real Element of ExtREAL
A is non empty complex-membered ext-real-membered real-membered interval Element of bool REAL
[.x,a.] is ext-real-membered interval set
inf A is ext-real Element of ExtREAL
A is non empty complex-membered ext-real-membered real-membered interval Element of bool REAL
inf A is ext-real Element of ExtREAL
x is ext-real Element of ExtREAL
a is ext-real Element of ExtREAL
[.x,a.[ is ext-real-membered non right_end interval set
a is ext-real Element of ExtREAL
x is ext-real Element of ExtREAL
A is non empty complex-membered ext-real-membered real-membered interval Element of bool REAL
].a,x.[ is complex-membered ext-real-membered real-membered non left_end non right_end interval Element of bool REAL
{ b1 where b1 is complex real ext-real Element of REAL : ( not b1 <= a & not x <= b1 ) } is set
sup A is ext-real Element of ExtREAL
A is non empty complex-membered ext-real-membered real-membered interval Element of bool REAL
sup A is ext-real Element of ExtREAL
x is ext-real Element of ExtREAL
a is ext-real Element of ExtREAL
].a,x.] is ext-real-membered non left_end interval set
a is ext-real Element of ExtREAL
x is ext-real Element of ExtREAL
A is non empty complex-membered ext-real-membered real-membered interval Element of bool REAL
[.a,x.] is ext-real-membered interval set
sup A is ext-real Element of ExtREAL
A is non empty complex-membered ext-real-membered real-membered interval Element of bool REAL
sup A is ext-real Element of ExtREAL
x is ext-real Element of ExtREAL
a is ext-real Element of ExtREAL
[.a,x.[ is ext-real-membered non right_end interval set
A is non empty complex-membered ext-real-membered real-membered interval Element of bool REAL
inf A is ext-real Element of ExtREAL
sup A is ext-real Element of ExtREAL
].(inf A),(sup A).[ is complex-membered ext-real-membered real-membered non left_end non right_end interval Element of bool REAL
{ b1 where b1 is complex real ext-real Element of REAL : ( not b1 <= inf A & not sup A <= b1 ) } is set
x is ext-real Element of ExtREAL
a is ext-real Element of ExtREAL
].x,a.[ is complex-membered ext-real-membered real-membered non left_end non right_end interval Element of bool REAL
{ b1 where b1 is complex real ext-real Element of REAL : ( not b1 <= x & not a <= b1 ) } is set
A is non empty complex-membered ext-real-membered real-membered interval Element of bool REAL
inf A is ext-real Element of ExtREAL
sup A is ext-real Element of ExtREAL
[.(inf A),(sup A).] is ext-real-membered interval set
x is complex real ext-real set
a is complex real ext-real set
[.x,a.] is complex-membered ext-real-membered real-membered interval closed Element of bool REAL
{ b1 where b1 is complex real ext-real Element of REAL : ( x <= b1 & b1 <= a ) } is set
a is ext-real Element of ExtREAL
A is non empty complex-membered ext-real-membered real-membered interval Element of bool REAL
inf A is ext-real Element of ExtREAL
sup A is ext-real Element of ExtREAL
[.(inf A),(sup A).[ is ext-real-membered non right_end interval set
x is complex real ext-real set
a is ext-real Element of ExtREAL
[.x,a.[ is complex-membered ext-real-membered real-membered non right_end interval Element of bool REAL
{ b1 where b1 is complex real ext-real Element of REAL : ( x <= b1 & not a <= b1 ) } is set
a is ext-real Element of ExtREAL
A is non empty complex-membered ext-real-membered real-membered interval Element of bool REAL
inf A is ext-real Element of ExtREAL
sup A is ext-real Element of ExtREAL
].(inf A),(sup A).] is ext-real-membered non left_end interval set
x is ext-real Element of ExtREAL
a is complex real ext-real set
].x,a.] is complex-membered ext-real-membered real-membered non left_end interval Element of bool REAL
{ b1 where b1 is complex real ext-real Element of REAL : ( not b1 <= x & b1 <= a ) } is set
a is ext-real Element of ExtREAL
A is non empty complex-membered ext-real-membered real-membered interval Element of bool REAL
x is non empty complex-membered ext-real-membered real-membered interval Element of bool REAL
sup A is ext-real Element of ExtREAL
inf x is ext-real Element of ExtREAL
a is complex real ext-real set
a is complex real ext-real set
(a) is ext-real Element of ExtREAL
(a) is ext-real Element of ExtREAL
x is complex-membered ext-real-membered real-membered set
A is complex-membered ext-real-membered real-membered set
x ++ A is complex-membered ext-real-membered real-membered set
{ K430(b1,b2) where b1, b2 is complex Element of COMPLEX : ( b1 in x & b2 in A ) } is set
x ++ A is ext-real-membered set
{ (b1 + b2) where b1, b2 is ext-real Element of ExtREAL : ( b1 in x & b2 in A ) } is set
a is complex real ext-real Element of REAL
a is complex Element of COMPLEX
c5 is complex Element of COMPLEX
a + c5 is set
r3 is complex real ext-real Element of REAL
x1 is complex real ext-real Element of REAL
n is complex real ext-real Element of REAL
m is complex real ext-real Element of REAL
n + m is complex real ext-real Element of REAL
a is complex real ext-real Element of REAL
c5 is complex real ext-real Element of REAL
a + c5 is complex real ext-real Element of REAL
A is non empty complex-membered ext-real-membered real-membered interval Element of bool REAL
sup A is ext-real Element of ExtREAL
x is non empty complex-membered ext-real-membered real-membered interval Element of bool REAL
inf x is ext-real Element of ExtREAL
A \/ x is non empty complex-membered ext-real-membered real-membered Element of bool REAL
A is complex-membered ext-real-membered real-membered set
x is complex real ext-real set
x ++ A is complex-membered ext-real-membered real-membered set
{x} is non empty finite complex-membered ext-real-membered real-membered left_end right_end bounded_below bounded_above real-bounded set
{x} ++ A is complex-membered ext-real-membered real-membered set
{ K430(b1,b2) where b1, b2 is complex Element of COMPLEX : ( b1 in {x} & b2 in A ) } is set
{x} ++ A is ext-real-membered set
{ (b1 + b2) where b1, b2 is ext-real Element of ExtREAL : ( b1 in {x} & b2 in A ) } is set
x ++ A is ext-real-membered set
A is complex-membered ext-real-membered real-membered set
x is complex real ext-real set
(A,x) is complex-membered ext-real-membered real-membered Element of bool REAL
{x} is non empty finite complex-membered ext-real-membered real-membered left_end right_end bounded_below bounded_above real-bounded set
{x} ++ A is complex-membered ext-real-membered real-membered set
{ K430(b1,b2) where b1, b2 is complex Element of COMPLEX : ( b1 in {x} & b2 in A ) } is set
{x} ++ A is ext-real-membered set
{ (b1 + b2) where b1, b2 is ext-real Element of ExtREAL : ( b1 in {x} & b2 in A ) } is set
x ++ A is ext-real-membered set
a is complex real ext-real Element of REAL
a is complex Element of COMPLEX
x + a is set
c5 is complex real ext-real Element of REAL
r3 is complex real ext-real Element of REAL
x + r3 is complex real ext-real Element of REAL
a is complex real ext-real Element of REAL
x + a is complex real ext-real Element of REAL
A is complex-membered ext-real-membered real-membered Element of bool REAL
x is complex real ext-real set
(A,x) is complex-membered ext-real-membered real-membered Element of bool REAL
{x} is non empty finite complex-membered ext-real-membered real-membered left_end right_end bounded_below bounded_above real-bounded set
{x} ++ A is complex-membered ext-real-membered real-membered set
{ K430(b1,b2) where b1, b2 is complex Element of COMPLEX : ( b1 in {x} & b2 in A ) } is set
{x} ++ A is ext-real-membered set
{ (b1 + b2) where b1, b2 is ext-real Element of ExtREAL : ( b1 in {x} & b2 in A ) } is set
x ++ A is ext-real-membered set
- x is complex real ext-real set
((A,x),(- x)) is complex-membered ext-real-membered real-membered Element of bool REAL
{(- x)} is non empty finite complex-membered ext-real-membered real-membered left_end right_end bounded_below bounded_above real-bounded set
{(- x)} ++ (A,x) is complex-membered ext-real-membered real-membered set
{ K430(b1,b2) where b1, b2 is complex Element of COMPLEX : ( b1 in {(- x)} & b2 in (A,x) ) } is set
{(- x)} ++ (A,x) is ext-real-membered set
{ (b1 + b2) where b1, b2 is ext-real Element of ExtREAL : ( b1 in {(- x)} & b2 in (A,x) ) } is set
(- x) ++ (A,x) is ext-real-membered set
a is set
a is complex real ext-real Element of REAL
c5 is complex real ext-real Element of REAL
(- x) + c5 is complex real ext-real Element of REAL
r3 is complex real ext-real Element of REAL
x + r3 is complex real ext-real Element of REAL
a is set
a is complex real ext-real set
a - (- x) is complex real ext-real set
- (- x) is complex real ext-real set
a + (- (- x)) is complex real ext-real set
c5 is complex real ext-real Element of REAL
c5 - x is complex real ext-real Element of REAL
c5 + (- x) is complex real ext-real set
r3 is complex real ext-real Element of REAL
(- x) + c5 is complex real ext-real Element of REAL
A is complex real ext-real set
x is complex-membered ext-real-membered real-membered Element of bool REAL
(x,A) is complex-membered ext-real-membered real-membered Element of bool REAL
{A} is non empty finite complex-membered ext-real-membered real-membered left_end right_end bounded_below bounded_above real-bounded set
{A} ++ x is complex-membered ext-real-membered real-membered set
{ K430(b1,b2) where b1, b2 is complex Element of COMPLEX : ( b1 in {A} & b2 in x ) } is set
{A} ++ x is ext-real-membered set
{ (b1 + b2) where b1, b2 is ext-real Element of ExtREAL : ( b1 in {A} & b2 in x ) } is set
A ++ x is ext-real-membered set
a is set
a is complex real ext-real Element of REAL
a - A is complex real ext-real Element of REAL
- A is complex real ext-real set
a + (- A) is complex real ext-real set
c5 is complex real ext-real Element of REAL
A + c5 is complex real ext-real Element of REAL
A is complex real ext-real set
({},A) is Relation-like non-zero empty-yielding RAT -valued epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural empty proper complex real ext-real non positive non negative finite finite-yielding V37() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V47() complex-valued ext-real-valued real-valued natural-valued bounded_below bounded_above real-bounded interval open_interval closed open integer Element of bool REAL
{A} is non empty finite complex-membered ext-real-membered real-membered left_end right_end bounded_below bounded_above real-bounded set
{A} ++ {} is Relation-like non-zero empty-yielding RAT -valued epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural empty complex real ext-real non positive non negative finite finite-yielding V37() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V47() complex-valued ext-real-valued real-valued natural-valued bounded_below bounded_above real-bounded interval integer set
{ K430(b1,b2) where b1, b2 is complex Element of COMPLEX : ( b1 in {A} & b2 in {} ) } is set
{A} ++ {} is Relation-like non-zero empty-yielding RAT -valued epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural empty complex real ext-real non positive non negative finite finite-yielding V37() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V47() complex-valued ext-real-valued real-valued natural-valued bounded_below bounded_above real-bounded interval integer set
{ (b1 + b2) where b1, b2 is ext-real Element of ExtREAL : ( b1 in {A} & b2 in {} ) } is set
A ++ {} is Relation-like non-zero empty-yielding RAT -valued epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural empty complex real ext-real non positive non negative finite finite-yielding V37() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V47() complex-valued ext-real-valued real-valued natural-valued bounded_below bounded_above real-bounded interval integer set
A is complex-membered ext-real-membered real-membered interval Element of bool REAL
x is complex real ext-real set
(A,x) is complex-membered ext-real-membered real-membered Element of bool REAL
{x} is non empty finite complex-membered ext-real-membered real-membered left_end right_end bounded_below bounded_above real-bounded set
{x} ++ A is complex-membered ext-real-membered real-membered set
{ K430(b1,b2) where b1, b2 is complex Element of COMPLEX : ( b1 in {x} & b2 in A ) } is set
{x} ++ A is ext-real-membered set
{ (b1 + b2) where b1, b2 is ext-real Element of ExtREAL : ( b1 in {x} & b2 in A ) } is set
x ++ A is ext-real-membered set
- x is complex real ext-real set
a is complex-membered ext-real-membered real-membered interval Element of bool REAL
c5 is complex real ext-real set
(a,c5) is complex-membered ext-real-membered real-membered Element of bool REAL
{c5} is non empty finite complex-membered ext-real-membered real-membered left_end right_end bounded_below bounded_above real-bounded set
{c5} ++ a is complex-membered ext-real-membered real-membered set
{ K430(b1,b2) where b1, b2 is complex Element of COMPLEX : ( b1 in {c5} & b2 in a ) } is set
{c5} ++ a is ext-real-membered set
{ (b1 + b2) where b1, b2 is ext-real Element of ExtREAL : ( b1 in {c5} & b2 in a ) } is set
c5 ++ a is ext-real-membered set
r3 is complex real ext-real Element of REAL
n is ext-real Element of ExtREAL
m is ext-real Element of ExtREAL
].n,m.[ is complex-membered ext-real-membered real-membered non left_end non right_end interval Element of bool REAL
{ b1 where b1 is complex real ext-real Element of REAL : ( not b1 <= n & not m <= b1 ) } is set
x1 is ext-real Element of ExtREAL
x1 + n is ext-real Element of ExtREAL
x1 + m is ext-real Element of ExtREAL
(a,r3) is complex-membered ext-real-membered real-membered Element of bool REAL
{r3} is non empty finite complex-membered ext-real-membered real-membered left_end right_end bounded_below bounded_above real-bounded set
{r3} ++ a is complex-membered ext-real-membered real-membered set
{ K430(b1,b2) where b1, b2 is complex Element of COMPLEX : ( b1 in {r3} & b2 in a ) } is set
{r3} ++ a is ext-real-membered set
{ (b1 + b2) where b1, b2 is ext-real Element of ExtREAL : ( b1 in {r3} & b2 in a ) } is set
r3 ++ a is ext-real-membered set
m1 is ext-real Element of ExtREAL
oi is ext-real Element of ExtREAL
].m1,oi.[ is complex-membered ext-real-membered real-membered non left_end non right_end interval Element of bool REAL
{ b1 where b1 is complex real ext-real Element of REAL : ( not b1 <= m1 & not oi <= b1 ) } is set
s is set
c is complex real ext-real Element of REAL
c1 is complex real ext-real Element of REAL
r3 + c1 is complex real ext-real Element of REAL
d1 is ext-real Element of ExtREAL
x1 + d1 is ext-real Element of ExtREAL
s is set
c is complex real ext-real Element of REAL
c - r3 is complex real ext-real Element of REAL
- r3 is complex real ext-real set
c + (- r3) is complex real ext-real set
r3 + (c - r3) is complex real ext-real Element of REAL
c1 is ext-real Element of ExtREAL
m + x1 is ext-real Element of ExtREAL
(m + x1) - x1 is ext-real Element of ExtREAL
- x1 is ext-real set
(m + x1) + (- x1) is ext-real set
c1 - x1 is ext-real Element of ExtREAL
c1 + (- x1) is ext-real set
n + x1 is ext-real Element of ExtREAL
(n + x1) - x1 is ext-real Element of ExtREAL
(n + x1) + (- x1) is ext-real set
a is complex-membered ext-real-membered real-membered interval Element of bool REAL
a is complex real ext-real Element of REAL
(a,a) is complex-membered ext-real-membered real-membered Element of bool REAL
{a} is non empty finite complex-membered ext-real-membered real-membered left_end right_end bounded_below bounded_above real-bounded set
{a} ++ a is complex-membered ext-real-membered real-membered set
{ K430(b1,b2) where b1, b2 is complex Element of COMPLEX : ( b1 in {a} & b2 in a ) } is set
{a} ++ a is ext-real-membered set
{ (b1 + b2) where b1, b2 is ext-real Element of ExtREAL : ( b1 in {a} & b2 in a ) } is set
a ++ a is ext-real-membered set
A is complex-membered ext-real-membered real-membered interval Element of bool REAL
x is complex real ext-real set
(A,x) is complex-membered ext-real-membered real-membered Element of bool REAL
{x} is non empty finite complex-membered ext-real-membered real-membered left_end right_end bounded_below bounded_above real-bounded set
{x} ++ A is complex-membered ext-real-membered real-membered set
{ K430(b1,b2) where b1, b2 is complex Element of COMPLEX : ( b1 in {x} & b2 in A ) } is set
{x} ++ A is ext-real-membered set
{ (b1 + b2) where b1, b2 is ext-real Element of ExtREAL : ( b1 in {x} & b2 in A ) } is set
x ++ A is ext-real-membered set
a is complex-membered ext-real-membered real-membered interval Element of bool REAL
a is complex real ext-real set
(a,a) is complex-membered ext-real-membered real-membered Element of bool REAL
{a} is non empty finite complex-membered ext-real-membered real-membered left_end right_end bounded_below bounded_above real-bounded set
{a} ++ a is complex-membered ext-real-membered real-membered set
{ K430(b1,b2) where b1, b2 is complex Element of COMPLEX : ( b1 in {a} & b2 in a ) } is set
{a} ++ a is ext-real-membered set
{ (b1 + b2) where b1, b2 is ext-real Element of ExtREAL : ( b1 in {a} & b2 in a ) } is set
a ++ a is ext-real-membered set
c5 is complex real ext-real Element of REAL
x1 is complex real ext-real set
n is complex real ext-real set
[.x1,n.] is complex-membered ext-real-membered real-membered interval closed Element of bool REAL
{ b1 where b1 is complex real ext-real Element of REAL : ( x1 <= b1 & b1 <= n ) } is set
r3 is ext-real Element of ExtREAL
m is ext-real Element of ExtREAL
r3 + m is ext-real Element of ExtREAL
m1 is ext-real Element of ExtREAL
r3 + m1 is ext-real Element of ExtREAL
(a,c5) is complex-membered ext-real-membered real-membered Element of bool REAL
{c5} is non empty finite complex-membered ext-real-membered real-membered left_end right_end bounded_below bounded_above real-bounded set
{c5} ++ a is complex-membered ext-real-membered real-membered set
{ K430(b1,b2) where b1, b2 is complex Element of COMPLEX : ( b1 in {c5} & b2 in a ) } is set
{c5} ++ a is ext-real-membered set
{ (b1 + b2) where b1, b2 is ext-real Element of ExtREAL : ( b1 in {c5} & b2 in a ) } is set
c5 ++ a is ext-real-membered set
oi is ext-real Element of ExtREAL
s is ext-real Element of ExtREAL
[.oi,s.] is ext-real-membered interval set
c is set
c1 is complex real ext-real Element of REAL
d1 is complex real ext-real Element of REAL
c5 + d1 is complex real ext-real Element of REAL
c is ext-real Element of ExtREAL
r3 + c is ext-real Element of ExtREAL
d1 is set
c is complex real ext-real Element of REAL
c - c5 is complex real ext-real Element of REAL
- c5 is complex real ext-real set
c + (- c5) is complex real ext-real set
c5 + (c - c5) is complex real ext-real Element of REAL
c1 is ext-real Element of ExtREAL
c1 is ext-real Element of ExtREAL
r3 + c1 is ext-real Element of ExtREAL
c1 - r3 is ext-real Element of ExtREAL
- r3 is ext-real set
c1 + (- r3) is ext-real set
c1 + r3 is ext-real Element of ExtREAL
(c1 + r3) - r3 is ext-real Element of ExtREAL
(c1 + r3) + (- r3) is ext-real set
c is ext-real Element of ExtREAL
r3 + c is ext-real Element of ExtREAL
c + r3 is ext-real Element of ExtREAL
(c + r3) - r3 is ext-real Element of ExtREAL
(c + r3) + (- r3) is ext-real set
- x is complex real ext-real set
a is complex-membered ext-real-membered real-membered interval Element of bool REAL
a is complex real ext-real Element of REAL
(a,a) is complex-membered ext-real-membered real-membered Element of bool REAL
{a} is non empty finite complex-membered ext-real-membered real-membered left_end right_end bounded_below bounded_above real-bounded set
{a} ++ a is complex-membered ext-real-membered real-membered set
{ K430(b1,b2) where b1, b2 is complex Element of COMPLEX : ( b1 in {a} & b2 in a ) } is set
{a} ++ a is ext-real-membered set
{ (b1 + b2) where b1, b2 is ext-real Element of ExtREAL : ( b1 in {a} & b2 in a ) } is set
a ++ a is ext-real-membered set
A is complex-membered ext-real-membered real-membered interval Element of bool REAL
x is complex real ext-real set
(A,x) is complex-membered ext-real-membered real-membered Element of bool REAL
{x} is non empty finite complex-membered ext-real-membered real-membered left_end right_end bounded_below bounded_above real-bounded set
{x} ++ A is complex-membered ext-real-membered real-membered set
{ K430(b1,b2) where b1, b2 is complex Element of COMPLEX : ( b1 in {x} & b2 in A ) } is set
{x} ++ A is ext-real-membered set
{ (b1 + b2) where b1, b2 is ext-real Element of ExtREAL : ( b1 in {x} & b2 in A ) } is set
x ++ A is ext-real-membered set
a is complex-membered ext-real-membered real-membered interval Element of bool REAL
a is complex real ext-real set
(a,a) is complex-membered ext-real-membered real-membered Element of bool REAL
{a} is non empty finite complex-membered ext-real-membered real-membered left_end right_end bounded_below bounded_above real-bounded set
{a} ++ a is complex-membered ext-real-membered real-membered set
{ K430(b1,b2) where b1, b2 is complex Element of COMPLEX : ( b1 in {a} & b2 in a ) } is set
{a} ++ a is ext-real-membered set
{ (b1 + b2) where b1, b2 is ext-real Element of ExtREAL : ( b1 in {a} & b2 in a ) } is set
a ++ a is ext-real-membered set
c5 is complex real ext-real Element of REAL
x1 is complex real ext-real set
n is ext-real Element of ExtREAL
[.x1,n.[ is complex-membered ext-real-membered real-membered non right_end interval Element of bool REAL
{ b1 where b1 is complex real ext-real Element of REAL : ( x1 <= b1 & not n <= b1 ) } is set
r3 is ext-real Element of ExtREAL
m is ext-real Element of ExtREAL
r3 + m is ext-real Element of ExtREAL
r3 + n is ext-real Element of ExtREAL
(a,c5) is complex-membered ext-real-membered real-membered Element of bool REAL
{c5} is non empty finite complex-membered ext-real-membered real-membered left_end right_end bounded_below bounded_above real-bounded set
{c5} ++ a is complex-membered ext-real-membered real-membered set
{ K430(b1,b2) where b1, b2 is complex Element of COMPLEX : ( b1 in {c5} & b2 in a ) } is set
{c5} ++ a is ext-real-membered set
{ (b1 + b2) where b1, b2 is ext-real Element of ExtREAL : ( b1 in {c5} & b2 in a ) } is set
c5 ++ a is ext-real-membered set
m1 is ext-real Element of ExtREAL
oi is ext-real Element of ExtREAL
[.m1,oi.[ is ext-real-membered non right_end interval set
s is set
c is complex real ext-real Element of REAL
c1 is complex real ext-real Element of REAL
c5 + c1 is complex real ext-real Element of REAL
d1 is ext-real Element of ExtREAL
r3 + d1 is ext-real Element of ExtREAL
s is set
c is complex real ext-real Element of REAL
c - c5 is complex real ext-real Element of REAL
- c5 is complex real ext-real set
c + (- c5) is complex real ext-real set
c5 + (c - c5) is complex real ext-real Element of REAL
c1 is ext-real Element of ExtREAL
n + r3 is ext-real Element of ExtREAL
(n + r3) - r3 is ext-real Element of ExtREAL
- r3 is ext-real set
(n + r3) + (- r3) is ext-real set
c1 - r3 is ext-real Element of ExtREAL
c1 + (- r3) is ext-real set
m + r3 is ext-real Element of ExtREAL
(m + r3) - r3 is ext-real Element of ExtREAL
(m + r3) + (- r3) is ext-real set
- x is complex real ext-real set
a is complex-membered ext-real-membered real-membered interval Element of bool REAL
a is complex real ext-real Element of REAL
(a,a) is complex-membered ext-real-membered real-membered Element of bool REAL
{a} is non empty finite complex-membered ext-real-membered real-membered left_end right_end bounded_below bounded_above real-bounded set
{a} ++ a is complex-membered ext-real-membered real-membered set
{ K430(b1,b2) where b1, b2 is complex Element of COMPLEX : ( b1 in {a} & b2 in a ) } is set
{a} ++ a is ext-real-membered set
{ (b1 + b2) where b1, b2 is ext-real Element of ExtREAL : ( b1 in {a} & b2 in a ) } is set
a ++ a is ext-real-membered set
A is complex-membered ext-real-membered real-membered interval Element of bool REAL
x is complex real ext-real set
(A,x) is complex-membered ext-real-membered real-membered Element of bool REAL
{x} is non empty finite complex-membered ext-real-membered real-membered left_end right_end bounded_below bounded_above real-bounded set
{x} ++ A is complex-membered ext-real-membered real-membered set
{ K430(b1,b2) where b1, b2 is complex Element of COMPLEX : ( b1 in {x} & b2 in A ) } is set
{x} ++ A is ext-real-membered set
{ (b1 + b2) where b1, b2 is ext-real Element of ExtREAL : ( b1 in {x} & b2 in A ) } is set
x ++ A is ext-real-membered set
a is complex-membered ext-real-membered real-membered interval Element of bool REAL
a is complex real ext-real set
(a,a) is complex-membered ext-real-membered real-membered Element of bool REAL
{a} is non empty finite complex-membered ext-real-membered real-membered left_end right_end bounded_below bounded_above real-bounded set
{a} ++ a is complex-membered ext-real-membered real-membered set
{ K430(b1,b2) where b1, b2 is complex Element of COMPLEX : ( b1 in {a} & b2 in a ) } is set
{a} ++ a is ext-real-membered set
{ (b1 + b2) where b1, b2 is ext-real Element of ExtREAL : ( b1 in {a} & b2 in a ) } is set
a ++ a is ext-real-membered set
c5 is complex real ext-real Element of REAL
x1 is ext-real Element of ExtREAL
n is complex real ext-real set
].x1,n.] is complex-membered ext-real-membered real-membered non left_end interval Element of bool REAL
{ b1 where b1 is complex real ext-real Element of REAL : ( not b1 <= x1 & b1 <= n ) } is set
r3 is ext-real Element of ExtREAL
r3 + x1 is ext-real Element of ExtREAL
m is ext-real Element of ExtREAL
r3 + m is ext-real Element of ExtREAL
(a,c5) is complex-membered ext-real-membered real-membered Element of bool REAL
{c5} is non empty finite complex-membered ext-real-membered real-membered left_end right_end bounded_below bounded_above real-bounded set
{c5} ++ a is complex-membered ext-real-membered real-membered set
{ K430(b1,b2) where b1, b2 is complex Element of COMPLEX : ( b1 in {c5} & b2 in a ) } is set
{c5} ++ a is ext-real-membered set
{ (b1 + b2) where b1, b2 is ext-real Element of ExtREAL : ( b1 in {c5} & b2 in a ) } is set
c5 ++ a is ext-real-membered set
].(r3 + x1),(r3 + m).] is ext-real-membered non left_end interval set
s is set
c is complex real ext-real Element of REAL
c1 is complex real ext-real Element of REAL
c5 + c1 is complex real ext-real Element of REAL
d1 is ext-real Element of ExtREAL
r3 + d1 is ext-real Element of ExtREAL
s is set
c is complex real ext-real Element of REAL
c - c5 is complex real ext-real Element of REAL
- c5 is complex real ext-real set
c + (- c5) is complex real ext-real set
c5 + (c - c5) is complex real ext-real Element of REAL
c1 is ext-real Element of ExtREAL
c1 - r3 is ext-real Element of ExtREAL
- r3 is ext-real set
c1 + (- r3) is ext-real set
m + r3 is ext-real Element of ExtREAL
(m + r3) - r3 is ext-real Element of ExtREAL
(m + r3) + (- r3) is ext-real set
x1 + r3 is ext-real Element of ExtREAL
(x1 + r3) - r3 is ext-real Element of ExtREAL
(x1 + r3) + (- r3) is ext-real set
- x is complex real ext-real set
a is complex-membered ext-real-membered real-membered interval Element of bool REAL
a is complex real ext-real Element of REAL
(a,a) is complex-membered ext-real-membered real-membered Element of bool REAL
{a} is non empty finite complex-membered ext-real-membered real-membered left_end right_end bounded_below bounded_above real-bounded set
{a} ++ a is complex-membered ext-real-membered real-membered set
{ K430(b1,b2) where b1, b2 is complex Element of COMPLEX : ( b1 in {a} & b2 in a ) } is set
{a} ++ a is ext-real-membered set
{ (b1 + b2) where b1, b2 is ext-real Element of ExtREAL : ( b1 in {a} & b2 in a ) } is set
a ++ a is ext-real-membered set
A is complex-membered ext-real-membered real-membered interval Element of bool REAL
x is complex real ext-real set
(A,x) is complex-membered ext-real-membered real-membered Element of bool REAL
{x} is non empty finite complex-membered ext-real-membered real-membered left_end right_end bounded_below bounded_above real-bounded set
{x} ++ A is complex-membered ext-real-membered real-membered set
{ K430(b1,b2) where b1, b2 is complex Element of COMPLEX : ( b1 in {x} & b2 in A ) } is set
{x} ++ A is ext-real-membered set
{ (b1 + b2) where b1, b2 is ext-real Element of ExtREAL : ( b1 in {x} & b2 in A ) } is set
x ++ A is ext-real-membered set
A is complex-membered ext-real-membered real-membered set
sup A is ext-real Element of ExtREAL
x is complex real ext-real set
(A,x) is complex-membered ext-real-membered real-membered Element of bool REAL
{x} is non empty finite complex-membered ext-real-membered real-membered left_end right_end bounded_below bounded_above real-bounded set
{x} ++ A is complex-membered ext-real-membered real-membered set
{ K430(b1,b2) where b1, b2 is complex Element of COMPLEX : ( b1 in {x} & b2 in A ) } is set
{x} ++ A is ext-real-membered set
{ (b1 + b2) where b1, b2 is ext-real Element of ExtREAL : ( b1 in {x} & b2 in A ) } is set
x ++ A is ext-real-membered set
sup (A,x) is ext-real Element of ExtREAL
a is ext-real Element of ExtREAL
a + (sup A) is ext-real Element of ExtREAL
a is ext-real UpperBound of (A,x)
c5 is ext-real Element of ExtREAL
c5 - a is ext-real Element of ExtREAL
- a is ext-real set
c5 + (- a) is ext-real set
r3 is ext-real set
x1 is ext-real Element of ExtREAL
a + x1 is ext-real Element of ExtREAL
n is complex real ext-real Element of REAL
x + n is complex real ext-real Element of REAL
a is ext-real set
c5 is complex real ext-real Element of REAL
x + c5 is complex real ext-real Element of REAL
r3 is ext-real Element of ExtREAL
a + r3 is ext-real Element of ExtREAL
x1 is complex set
n is complex set
x1 + n is set
A is complex-membered ext-real-membered real-membered set
inf A is ext-real Element of ExtREAL
x is complex real ext-real set
(A,x) is complex-membered ext-real-membered real-membered Element of bool REAL
{x} is non empty finite complex-membered ext-real-membered real-membered left_end right_end bounded_below bounded_above real-bounded set
{x} ++ A is complex-membered ext-real-membered real-membered set
{ K430(b1,b2) where b1, b2 is complex Element of COMPLEX : ( b1 in {x} & b2 in A ) } is set
{x} ++ A is ext-real-membered set
{ (b1 + b2) where b1, b2 is ext-real Element of ExtREAL : ( b1 in {x} & b2 in A ) } is set
x ++ A is ext-real-membered set
inf (A,x) is ext-real Element of ExtREAL
a is ext-real Element of ExtREAL
a + (inf A) is ext-real Element of ExtREAL
a is ext-real LowerBound of (A,x)
c5 is ext-real Element of ExtREAL
c5 - a is ext-real Element of ExtREAL
- a is ext-real set
c5 + (- a) is ext-real set
r3 is ext-real set
x1 is ext-real Element of ExtREAL
a + x1 is ext-real Element of ExtREAL
n is complex real ext-real Element of REAL
x + n is complex real ext-real Element of REAL
a is ext-real set
c5 is complex real ext-real Element of REAL
x + c5 is complex real ext-real Element of REAL
r3 is ext-real Element of ExtREAL
a + r3 is ext-real Element of ExtREAL
x1 is complex set
n is complex set
x1 + n is set
A is complex-membered ext-real-membered real-membered interval Element of bool REAL
diameter A is ext-real Element of ExtREAL
x is complex real ext-real set
(A,x) is complex-membered ext-real-membered real-membered Element of bool REAL
{x} is non empty finite complex-membered ext-real-membered real-membered left_end right_end bounded_below bounded_above real-bounded set
{x} ++ A is complex-membered ext-real-membered real-membered set
{ K430(b1,b2) where b1, b2 is complex Element of COMPLEX : ( b1 in {x} & b2 in A ) } is set
{x} ++ A is ext-real-membered set
{ (b1 + b2) where b1, b2 is ext-real Element of ExtREAL : ( b1 in {x} & b2 in A ) } is set
x ++ A is ext-real-membered set
diameter (A,x) is ext-real Element of ExtREAL
a is complex real ext-real set
a is complex real ext-real Element of REAL
x + a is complex real ext-real Element of REAL
sup A is ext-real Element of ExtREAL
inf A is ext-real Element of ExtREAL
(sup A) - (inf A) is ext-real Element of ExtREAL
- (inf A) is ext-real set
(sup A) + (- (inf A)) is ext-real set
c5 is ext-real Element of ExtREAL
c5 + (sup A) is ext-real Element of ExtREAL
c5 + (inf A) is ext-real Element of ExtREAL
(c5 + (sup A)) - (c5 + (inf A)) is ext-real Element of ExtREAL
- (c5 + (inf A)) is ext-real set
(c5 + (sup A)) + (- (c5 + (inf A))) is ext-real set
sup (A,x) is ext-real Element of ExtREAL
(sup (A,x)) - (c5 + (inf A)) is ext-real Element of ExtREAL
(sup (A,x)) + (- (c5 + (inf A))) is ext-real set
inf (A,x) is ext-real Element of ExtREAL
(sup (A,x)) - (inf (A,x)) is ext-real Element of ExtREAL
- (inf (A,x)) is ext-real set
(sup (A,x)) + (- (inf (A,x))) is ext-real set
A is set
{1} is non empty finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end right_end bounded_below bounded_above real-bounded with_non-empty_elements non empty-membered Element of bool REAL
{1} is non empty finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end right_end bounded_below bounded_above real-bounded with_non-empty_elements non empty-membered Element of bool REAL
A is set
x is set
meet x is set
a is set
a is set
{a} is non empty finite set
a \/ {a} is non empty set
c5 is set
r3 is set
c5 is set
c5 is set
r3 is set
x1 is set
r3 is set
x1 is set
a is set
a is set
a is set
c5 is set
A is set
bool A is non empty set
bool (bool A) is non empty set
x is Element of bool (bool A)
A is non empty set
x is non empty set
[:A,x:] is Relation-like non empty set
bool [:A,x:] is non empty set
a is Relation-like A -defined x -valued non empty Function-like total V30(A,x) Element of bool [:A,x:]
a .: A is Element of bool x
bool x is non empty set
the Element of A is Element of A
dom a is non empty Element of bool A
bool A is non empty set
A is set
x is set
[:A,x:] is Relation-like set
bool [:A,x:] is non empty set
bool x is non empty Element of bool (bool x)
bool x is non empty set
bool (bool x) is non empty set
bool A is non empty Element of bool (bool A)
bool A is non empty set
bool (bool A) is non empty set
[:(bool x),(bool A):] is Relation-like non empty set
bool [:(bool x),(bool A):] is non empty set
a is Relation-like A -defined x -valued Function-like V30(A,x) Element of bool [:A,x:]
x is set
bool x is non empty set
bool (bool x) is non empty set
A is set
[:A,x:] is Relation-like set
bool [:A,x:] is non empty set
a is set
bool x is non empty Element of bool (bool x)
bool A is non empty Element of bool (bool A)
bool A is non empty set
bool (bool A) is non empty set
a is Element of bool (bool x)
meet a is Element of bool x
c5 is Relation-like A -defined x -valued Function-like V30(A,x) Element of bool [:A,x:]
(A,x,c5) is Relation-like bool x -defined bool A -valued non empty Function-like total V30( bool x, bool A) Element of bool [:(bool x),(bool A):]
[:(bool x),(bool A):] is Relation-like non empty set
bool [:(bool x),(bool A):] is non empty set
(A,x,c5) .: a is Element of bool (bool A)
bool (bool A) is non empty set
meet ((A,x,c5) .: a) is Element of bool A
c5 . a is set
r3 is set
(A,x,c5) . r3 is set
c5 " r3 is Element of bool A
A is complex real ext-real set
abs A is complex real ext-real Element of REAL
x is complex real ext-real set
abs x is complex real ext-real Element of REAL
(abs A) + (abs x) is complex real ext-real Element of REAL
A is complex real ext-real set
abs A is complex real ext-real Element of REAL
x is complex real ext-real set
abs x is complex real ext-real Element of REAL
a is complex real ext-real set
abs a is complex real ext-real Element of REAL
(abs A) + (abs a) is complex real ext-real Element of REAL
- A is complex real ext-real set
- x is complex real ext-real set
(- A) + (abs a) is complex real ext-real Element of REAL
(- x) + 0 is complex real ext-real Element of REAL
a + (abs A) is complex real ext-real Element of REAL
x + 0 is complex real ext-real Element of REAL
A is Relation-like NAT -defined REAL -valued non empty Function-like total V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
lim A is complex real ext-real Element of REAL
A " is Relation-like NAT -defined REAL -valued non empty Function-like total V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
x is complex real ext-real set
a is complex real ext-real set
abs x is complex real ext-real Element of REAL
abs a is complex real ext-real Element of REAL
(abs x) + (abs a) is complex real ext-real Element of REAL
1 / ((abs x) + (abs a)) is complex real ext-real Element of REAL
((abs x) + (abs a)) " is complex real ext-real set
1 * (((abs x) + (abs a)) ") is complex real ext-real set
x1 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below integer V90() Element of NAT
A . x1 is complex real ext-real Element of ExtREAL
(A ") . x1 is complex real ext-real Element of ExtREAL
abs ((A ") . x1) is complex real ext-real Element of REAL
1 / (A . x1) is complex real ext-real Element of REAL
(A . x1) " is complex real ext-real set
1 * ((A . x1) ") is complex real ext-real set
abs (A . x1) is complex real ext-real Element of REAL
1 / (abs (A . x1)) is complex real ext-real Element of REAL
(abs (A . x1)) " is complex real ext-real set
1 * ((abs (A . x1)) ") is complex real ext-real set
((A ") . x1) " is complex real ext-real set
((A . x1) ") " is complex real ext-real set
(abs ((A ") . x1)) " is complex real ext-real Element of REAL
((abs x) + (abs a)) " is complex real ext-real Element of REAL
(A ") . 1 is complex real ext-real Element of ExtREAL
x1 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below integer V90() Element of NAT
A . x1 is complex real ext-real Element of ExtREAL
(A . x1) - 0 is complex real ext-real Element of REAL
- 0 is Relation-like non-zero empty-yielding RAT -valued epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural empty complex real ext-real non positive non negative finite finite-yielding V37() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V47() complex-valued ext-real-valued real-valued natural-valued bounded_below bounded_above real-bounded interval integer set
(A . x1) + (- 0) is complex real ext-real set
abs ((A . x1) - 0) is complex real ext-real Element of REAL
A is Relation-like NAT -defined REAL -valued non empty Function-like total V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
rng A is non empty complex-membered ext-real-membered real-membered Element of bool REAL
x is complex real ext-real set
a is complex real ext-real set
a + 1 is complex real ext-real Element of REAL
a is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below integer V90() Element of NAT
A . a is complex real ext-real Element of REAL
A . a is complex real ext-real Element of ExtREAL
x - 1 is complex real ext-real Element of REAL
- 1 is complex real ext-real non positive integer set
x + (- 1) is complex real ext-real set
a is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below integer V90() Element of NAT
A . a is complex real ext-real Element of REAL
x + 1 is complex real ext-real Element of REAL
A . a is complex real ext-real Element of ExtREAL
x is complex real ext-real set
a is complex real ext-real set
a is ext-real set
dom A is non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end bounded_below Element of bool NAT
c5 is set
A . c5 is complex real ext-real Element of ExtREAL
a is ext-real set
dom A is non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end bounded_below Element of bool NAT
c5 is set
A . c5 is complex real ext-real Element of ExtREAL
A is complex-membered ext-real-membered real-membered set
upper_bound A is complex real ext-real set
x is non empty complex-membered ext-real-membered real-membered bounded_above set
upper_bound x is complex real ext-real set
sup x is complex real ext-real set
x is non empty complex-membered ext-real-membered real-membered bounded_above set
upper_bound x is complex real ext-real set
sup x is complex real ext-real set
lower_bound A is complex real ext-real set
x is non empty complex-membered ext-real-membered real-membered bounded_below set
lower_bound x is complex real ext-real set
inf x is complex real ext-real set
x is non empty complex-membered ext-real-membered real-membered bounded_below set
lower_bound x is complex real ext-real set
inf x is complex real ext-real set
[.0,0.] is non empty complex-membered ext-real-membered real-membered interval closed Element of bool REAL
{ b1 where b1 is complex real ext-real Element of REAL : ( 0 <= b1 & b1 <= 0 ) } is set
{0} is non empty finite V37() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end right_end bounded_below bounded_above real-bounded Element of bool REAL
bool (bool REAL) is non empty set
A is complex-membered ext-real-membered real-membered Element of bool REAL
-- A is complex-membered ext-real-membered real-membered set
{ K428(b1) where b1 is complex Element of COMPLEX : b1 in A } is set
-- A is ext-real-membered set
{ (- b1) where b1 is ext-real Element of ExtREAL : b1 in A } is set
A is complex real ext-real set
x is complex-membered ext-real-membered real-membered Element of bool REAL
- A is complex real ext-real set
(x) is complex-membered ext-real-membered real-membered Element of bool REAL
{ K428(b1) where b1 is complex Element of COMPLEX : b1 in x } is set
-- x is ext-real-membered set
{ (- b1) where b1 is ext-real Element of ExtREAL : b1 in x } is set
a is complex real ext-real set
- a is complex real ext-real set
a is complex-membered ext-real-membered real-membered Element of bool REAL
(a) is complex-membered ext-real-membered real-membered Element of bool REAL
{ K428(b1) where b1 is complex Element of COMPLEX : b1 in a } is set
-- a is ext-real-membered set
{ (- b1) where b1 is ext-real Element of ExtREAL : b1 in a } is set
A is complex-membered ext-real-membered real-membered Element of bool REAL
(A) is complex-membered ext-real-membered real-membered Element of bool REAL
{ K428(b1) where b1 is complex Element of COMPLEX : b1 in A } is set
-- A is ext-real-membered set
{ (- b1) where b1 is ext-real Element of ExtREAL : b1 in A } is set
x is complex real ext-real set
- x is complex real ext-real set
a is ext-real set
a is complex Element of COMPLEX
- a is complex set
c5 is complex real ext-real Element of REAL
A is complex-membered ext-real-membered real-membered Element of bool REAL
(A) is complex-membered ext-real-membered real-membered Element of bool REAL
{ K428(b1) where b1 is complex Element of COMPLEX : b1 in A } is set
-- A is ext-real-membered set
{ (- b1) where b1 is ext-real Element of ExtREAL : b1 in A } is set
x is complex real ext-real set
- x is complex real ext-real set
a is ext-real set
a is complex Element of COMPLEX
- a is complex set
c5 is complex real ext-real Element of REAL
A is complex-membered ext-real-membered real-membered Element of bool REAL
(A) is complex-membered ext-real-membered real-membered Element of bool REAL
{ K428(b1) where b1 is complex Element of COMPLEX : b1 in A } is set
-- A is ext-real-membered set
{ (- b1) where b1 is ext-real Element of ExtREAL : b1 in A } is set
((A)) is complex-membered ext-real-membered real-membered Element of bool REAL
{ K428(b1) where b1 is complex Element of COMPLEX : b1 in (A) } is set
-- (A) is ext-real-membered set
{ (- b1) where b1 is ext-real Element of ExtREAL : b1 in (A) } is set
A is complex-membered ext-real-membered real-membered Element of bool REAL
(A) is complex-membered ext-real-membered real-membered Element of bool REAL
{ K428(b1) where b1 is complex Element of COMPLEX : b1 in A } is set
-- A is ext-real-membered set
{ (- b1) where b1 is ext-real Element of ExtREAL : b1 in A } is set
((A)) is complex-membered ext-real-membered real-membered Element of bool REAL
{ K428(b1) where b1 is complex Element of COMPLEX : b1 in (A) } is set
-- (A) is ext-real-membered set
{ (- b1) where b1 is ext-real Element of ExtREAL : b1 in (A) } is set
A is non empty complex-membered ext-real-membered real-membered Element of bool REAL
lower_bound A is complex real ext-real Element of REAL
(A) is non empty complex-membered ext-real-membered real-membered Element of bool REAL
{ K428(b1) where b1 is complex Element of COMPLEX : b1 in A } is set
-- A is non empty ext-real-membered set
{ (- b1) where b1 is ext-real Element of ExtREAL : b1 in A } is set
upper_bound (A) is complex real ext-real Element of REAL
- (upper_bound (A)) is complex real ext-real Element of REAL
a is complex real ext-real set
a is complex real ext-real set
- a is complex real ext-real set
((A)) is non empty complex-membered ext-real-membered real-membered Element of bool REAL
{ K428(b1) where b1 is complex Element of COMPLEX : b1 in (A) } is set
-- (A) is non empty ext-real-membered set
{ (- b1) where b1 is ext-real Element of ExtREAL : b1 in (A) } is set
- (- a) is complex real ext-real set
- a is complex real ext-real set
- (- (upper_bound (A))) is complex real ext-real Element of REAL
a is complex real ext-real set
- a is complex real ext-real set
A is non empty complex-membered ext-real-membered real-membered Element of bool REAL
upper_bound A is complex real ext-real Element of REAL
(A) is non empty complex-membered ext-real-membered real-membered Element of bool REAL
{ K428(b1) where b1 is complex Element of COMPLEX : b1 in A } is set
-- A is non empty ext-real-membered set
{ (- b1) where b1 is ext-real Element of ExtREAL : b1 in A } is set
lower_bound (A) is complex real ext-real Element of REAL
- (lower_bound (A)) is complex real ext-real Element of REAL
a is complex real ext-real set
a is complex real ext-real set
- a is complex real ext-real set
((A)) is non empty complex-membered ext-real-membered real-membered Element of bool REAL
{ K428(b1) where b1 is complex Element of COMPLEX : b1 in (A) } is set
-- (A) is non empty ext-real-membered set
{ (- b1) where b1 is ext-real Element of ExtREAL : b1 in (A) } is set
- a is complex real ext-real set
- (- a) is complex real ext-real set
- (- (lower_bound (A))) is complex real ext-real Element of REAL
a is complex real ext-real set
- a is complex real ext-real set
A is complex-membered ext-real-membered real-membered Element of bool REAL
(A) is complex-membered ext-real-membered real-membered Element of bool REAL
{ K428(b1) where b1 is complex Element of COMPLEX : b1 in A } is set
-- A is ext-real-membered set
{ (- b1) where b1 is ext-real Element of ExtREAL : b1 in A } is set
x is Relation-like NAT -defined REAL -valued non empty Function-like total V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
rng x is non empty complex-membered ext-real-membered real-membered set
lim x is complex real ext-real Element of REAL
rng x is non empty complex-membered ext-real-membered real-membered Element of bool REAL
- (lim x) is complex real ext-real Element of REAL
- x is Relation-like NAT -defined REAL -valued non empty Function-like total V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
- 1 is complex real ext-real non positive integer set
(- 1) * x is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
lim (- x) is complex real ext-real Element of REAL
rng (- x) is non empty complex-membered ext-real-membered real-membered Element of bool REAL
a is set
dom (- x) is non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end bounded_below Element of bool NAT
a is set
(- x) . a is complex real ext-real Element of ExtREAL
c5 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below integer V90() Element of NAT
x . c5 is complex real ext-real Element of ExtREAL
- (x . c5) is complex real ext-real Element of ExtREAL
- (x . c5) is complex real ext-real set
((A)) is complex-membered ext-real-membered real-membered Element of bool REAL
{ K428(b1) where b1 is complex Element of COMPLEX : b1 in (A) } is set
-- (A) is ext-real-membered set
{ (- b1) where b1 is ext-real Element of ExtREAL : b1 in (A) } is set
- (- (lim x)) is complex real ext-real Element of REAL
A is complex-membered ext-real-membered real-membered Element of bool REAL
(A) is complex-membered ext-real-membered real-membered Element of bool REAL
{ K428(b1) where b1 is complex Element of COMPLEX : b1 in A } is set
-- A is ext-real-membered set
{ (- b1) where b1 is ext-real Element of ExtREAL : b1 in A } is set
((A)) is complex-membered ext-real-membered real-membered Element of bool REAL
{ K428(b1) where b1 is complex Element of COMPLEX : b1 in (A) } is set
-- (A) is ext-real-membered set
{ (- b1) where b1 is ext-real Element of ExtREAL : b1 in (A) } is set
A is complex-membered ext-real-membered real-membered Element of bool REAL
x is complex real ext-real Element of REAL
(A,x) is complex-membered ext-real-membered real-membered Element of bool REAL
{x} is non empty finite complex-membered ext-real-membered real-membered left_end right_end bounded_below bounded_above real-bounded set
{x} ++ A is complex-membered ext-real-membered real-membered set
{ K430(b1,b2) where b1, b2 is complex Element of COMPLEX : ( b1 in {x} & b2 in A ) } is set
{x} ++ A is ext-real-membered set
{ (b1 + b2) where b1, b2 is ext-real Element of ExtREAL : ( b1 in {x} & b2 in A ) } is set
x ++ A is ext-real-membered set
{ (x + b1) where b1 is complex real ext-real Element of REAL : b1 in A } is set
a is set
a is complex real ext-real Element of REAL
c5 is complex real ext-real Element of REAL
x + c5 is complex real ext-real Element of REAL
a is set
a is complex real ext-real Element of REAL
x + a is complex real ext-real Element of REAL
A is complex real ext-real set
x is complex-membered ext-real-membered real-membered Element of bool REAL
a is complex real ext-real Element of REAL
a + A is complex real ext-real Element of REAL
(x,a) is complex-membered ext-real-membered real-membered Element of bool REAL
{a} is non empty finite complex-membered ext-real-membered real-membered left_end right_end bounded_below bounded_above real-bounded set
{a} ++ x is complex-membered ext-real-membered real-membered set
{ K430(b1,b2) where b1, b2 is complex Element of COMPLEX : ( b1 in {a} & b2 in x ) } is set
{a} ++ x is ext-real-membered set
{ (b1 + b2) where b1, b2 is ext-real Element of ExtREAL : ( b1 in {a} & b2 in x ) } is set
a ++ x is ext-real-membered set
{ (a + b1) where b1 is complex real ext-real Element of REAL : b1 in x } is set
a is complex real ext-real Element of REAL
a + a is complex real ext-real Element of REAL
A is complex-membered ext-real-membered real-membered Element of bool REAL
(A,0) is complex-membered ext-real-membered real-membered Element of bool REAL
{0} is non empty finite V37() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end right_end bounded_below bounded_above real-bounded set
{0} ++ A is complex-membered ext-real-membered real-membered set
{ K430(b1,b2) where b1, b2 is complex Element of COMPLEX : ( b1 in {0} & b2 in A ) } is set
{0} ++ A is ext-real-membered set
{ (b1 + b2) where b1, b2 is ext-real Element of ExtREAL : ( b1 in {0} & b2 in A ) } is set
0 ++ A is ext-real-membered set
A is complex-membered ext-real-membered real-membered Element of bool REAL
a is complex real ext-real Element of REAL
(A,a) is complex-membered ext-real-membered real-membered Element of bool REAL
{a} is non empty finite complex-membered ext-real-membered real-membered left_end right_end bounded_below bounded_above real-bounded set
{a} ++ A is complex-membered ext-real-membered real-membered set
{ K430(b1,b2) where b1, b2 is complex Element of COMPLEX : ( b1 in {a} & b2 in A ) } is set
{a} ++ A is ext-real-membered set
{ (b1 + b2) where b1, b2 is ext-real Element of ExtREAL : ( b1 in {a} & b2 in A ) } is set
a ++ A is ext-real-membered set
x is complex real ext-real Element of REAL
((A,a),x) is complex-membered ext-real-membered real-membered Element of bool REAL
{x} is non empty finite complex-membered ext-real-membered real-membered left_end right_end bounded_below bounded_above real-bounded set
{x} ++ (A,a) is complex-membered ext-real-membered real-membered set
{ K430(b1,b2) where b1, b2 is complex Element of COMPLEX : ( b1 in {x} & b2 in (A,a) ) } is set
{x} ++ (A,a) is ext-real-membered set
{ (b1 + b2) where b1, b2 is ext-real Element of ExtREAL : ( b1 in {x} & b2 in (A,a) ) } is set
x ++ (A,a) is ext-real-membered set
x + a is complex real ext-real Element of REAL
(A,(x + a)) is complex-membered ext-real-membered real-membered Element of bool REAL
{(x + a)} is non empty finite complex-membered ext-real-membered real-membered left_end right_end bounded_below bounded_above real-bounded set
{(x + a)} ++ A is complex-membered ext-real-membered real-membered set
{ K430(b1,b2) where b1, b2 is complex Element of COMPLEX : ( b1 in {(x + a)} & b2 in A ) } is set
{(x + a)} ++ A is ext-real-membered set
{ (b1 + b2) where b1, b2 is ext-real Element of ExtREAL : ( b1 in {(x + a)} & b2 in A ) } is set
(x + a) ++ A is ext-real-membered set
A is complex-membered ext-real-membered real-membered Element of bool REAL
x is complex real ext-real Element of REAL
(A,x) is complex-membered ext-real-membered real-membered Element of bool REAL
{x} is non empty finite complex-membered ext-real-membered real-membered left_end right_end bounded_below bounded_above real-bounded set
{x} ++ A is complex-membered ext-real-membered real-membered set
{ K430(b1,b2) where b1, b2 is complex Element of COMPLEX : ( b1 in {x} & b2 in A ) } is set
{x} ++ A is ext-real-membered set
{ (b1 + b2) where b1, b2 is ext-real Element of ExtREAL : ( b1 in {x} & b2 in A ) } is set
x ++ A is ext-real-membered set
a is complex real ext-real set
x + a is complex real ext-real Element of REAL
a is ext-real set
{ (x + b1) where b1 is complex real ext-real Element of REAL : b1 in A } is set
c5 is complex real ext-real Element of REAL
x + c5 is complex real ext-real Element of REAL
A is complex-membered ext-real-membered real-membered Element of bool REAL
x is complex real ext-real Element of REAL
(A,x) is complex-membered ext-real-membered real-membered Element of bool REAL
{x} is non empty finite complex-membered ext-real-membered real-membered left_end right_end bounded_below bounded_above real-bounded set
{x} ++ A is complex-membered ext-real-membered real-membered set
{ K430(b1,b2) where b1, b2 is complex Element of COMPLEX : ( b1 in {x} & b2 in A ) } is set
{x} ++ A is ext-real-membered set
{ (b1 + b2) where b1, b2 is ext-real Element of ExtREAL : ( b1 in {x} & b2 in A ) } is set
x ++ A is ext-real-membered set
- x is complex real ext-real Element of REAL
((A,x),(- x)) is complex-membered ext-real-membered real-membered Element of bool REAL
{(- x)} is non empty finite complex-membered ext-real-membered real-membered left_end right_end bounded_below bounded_above real-bounded set
{(- x)} ++ (A,x) is complex-membered ext-real-membered real-membered set
{ K430(b1,b2) where b1, b2 is complex Element of COMPLEX : ( b1 in {(- x)} & b2 in (A,x) ) } is set
{(- x)} ++ (A,x) is ext-real-membered set
{ (b1 + b2) where b1, b2 is ext-real Element of ExtREAL : ( b1 in {(- x)} & b2 in (A,x) ) } is set
(- x) ++ (A,x) is ext-real-membered set
(- x) + x is complex real ext-real Element of REAL
(A,((- x) + x)) is complex-membered ext-real-membered real-membered Element of bool REAL
{((- x) + x)} is non empty finite complex-membered ext-real-membered real-membered left_end right_end bounded_below bounded_above real-bounded set
{((- x) + x)} ++ A is complex-membered ext-real-membered real-membered set
{ K430(b1,b2) where b1, b2 is complex Element of COMPLEX : ( b1 in {((- x) + x)} & b2 in A ) } is set
{((- x) + x)} ++ A is ext-real-membered set
{ (b1 + b2) where b1, b2 is ext-real Element of ExtREAL : ( b1 in {((- x) + x)} & b2 in A ) } is set
((- x) + x) ++ A is ext-real-membered set
A is complex-membered ext-real-membered real-membered Element of bool REAL
x is complex real ext-real Element of REAL
(A,x) is complex-membered ext-real-membered real-membered Element of bool REAL
{x} is non empty finite complex-membered ext-real-membered real-membered left_end right_end bounded_below bounded_above real-bounded set
{x} ++ A is complex-membered ext-real-membered real-membered set
{ K430(b1,b2) where b1, b2 is complex Element of COMPLEX : ( b1 in {x} & b2 in A ) } is set
{x} ++ A is ext-real-membered set
{ (b1 + b2) where b1, b2 is ext-real Element of ExtREAL : ( b1 in {x} & b2 in A ) } is set
x ++ A is ext-real-membered set
a is complex real ext-real set
x + a is complex real ext-real Element of REAL
a is ext-real set
{ (x + b1) where b1 is complex real ext-real Element of REAL : b1 in A } is set
c5 is complex real ext-real Element of REAL
x + c5 is complex real ext-real Element of REAL
A is complex-membered ext-real-membered real-membered Element of bool REAL
x is complex real ext-real Element of REAL
(A,x) is complex-membered ext-real-membered real-membered Element of bool REAL
{x} is non empty finite complex-membered ext-real-membered real-membered left_end right_end bounded_below bounded_above real-bounded set
{x} ++ A is complex-membered ext-real-membered real-membered set
{ K430(b1,b2) where b1, b2 is complex Element of COMPLEX : ( b1 in {x} & b2 in A ) } is set
{x} ++ A is ext-real-membered set
{ (b1 + b2) where b1, b2 is ext-real Element of ExtREAL : ( b1 in {x} & b2 in A ) } is set
x ++ A is ext-real-membered set
- x is complex real ext-real Element of REAL
((A,x),(- x)) is complex-membered ext-real-membered real-membered Element of bool REAL
{(- x)} is non empty finite complex-membered ext-real-membered real-membered left_end right_end bounded_below bounded_above real-bounded set
{(- x)} ++ (A,x) is complex-membered ext-real-membered real-membered set
{ K430(b1,b2) where b1, b2 is complex Element of COMPLEX : ( b1 in {(- x)} & b2 in (A,x) ) } is set
{(- x)} ++ (A,x) is ext-real-membered set
{ (b1 + b2) where b1, b2 is ext-real Element of ExtREAL : ( b1 in {(- x)} & b2 in (A,x) ) } is set
(- x) ++ (A,x) is ext-real-membered set
(- x) + x is complex real ext-real Element of REAL
(A,((- x) + x)) is complex-membered ext-real-membered real-membered Element of bool REAL
{((- x) + x)} is non empty finite complex-membered ext-real-membered real-membered left_end right_end bounded_below bounded_above real-bounded set
{((- x) + x)} ++ A is complex-membered ext-real-membered real-membered set
{ K430(b1,b2) where b1, b2 is complex Element of COMPLEX : ( b1 in {((- x) + x)} & b2 in A ) } is set
{((- x) + x)} ++ A is ext-real-membered set
{ (b1 + b2) where b1, b2 is ext-real Element of ExtREAL : ( b1 in {((- x) + x)} & b2 in A ) } is set
((- x) + x) ++ A is ext-real-membered set
A is complex real ext-real Element of REAL
x is non empty complex-membered ext-real-membered real-membered Element of bool REAL
(x,A) is non empty complex-membered ext-real-membered real-membered Element of bool REAL
{A} is non empty finite complex-membered ext-real-membered real-membered left_end right_end bounded_below bounded_above real-bounded set
{A} ++ x is non empty complex-membered ext-real-membered real-membered set
{ K430(b1,b2) where b1, b2 is complex Element of COMPLEX : ( b1 in {A} & b2 in x ) } is set
{A} ++ x is non empty ext-real-membered set
{ (b1 + b2) where b1, b2 is ext-real Element of ExtREAL : ( b1 in {A} & b2 in x ) } is set
A ++ x is non empty ext-real-membered set
lower_bound (x,A) is complex real ext-real Element of REAL
lower_bound x is complex real ext-real Element of REAL
A + (lower_bound x) is complex real ext-real Element of REAL
a is complex real ext-real set
c5 is complex real ext-real set
A + c5 is complex real ext-real Element of REAL
a - A is complex real ext-real Element of REAL
- A is complex real ext-real set
a + (- A) is complex real ext-real set
a is complex real ext-real set
{ (A + b1) where b1 is complex real ext-real Element of REAL : b1 in x } is set
c5 is complex real ext-real Element of REAL
A + c5 is complex real ext-real Element of REAL
A is complex real ext-real Element of REAL
x is non empty complex-membered ext-real-membered real-membered Element of bool REAL
(x,A) is non empty complex-membered ext-real-membered real-membered Element of bool REAL
{A} is non empty finite complex-membered ext-real-membered real-membered left_end right_end bounded_below bounded_above real-bounded set
{A} ++ x is non empty complex-membered ext-real-membered real-membered set
{ K430(b1,b2) where b1, b2 is complex Element of COMPLEX : ( b1 in {A} & b2 in x ) } is set
{A} ++ x is non empty ext-real-membered set
{ (b1 + b2) where b1, b2 is ext-real Element of ExtREAL : ( b1 in {A} & b2 in x ) } is set
A ++ x is non empty ext-real-membered set
upper_bound (x,A) is complex real ext-real Element of REAL
upper_bound x is complex real ext-real Element of REAL
A + (upper_bound x) is complex real ext-real Element of REAL
a is complex real ext-real set
c5 is complex real ext-real set
A + c5 is complex real ext-real Element of REAL
a - A is complex real ext-real Element of REAL
- A is complex real ext-real set
a + (- A) is complex real ext-real set
a is complex real ext-real set
{ (A + b1) where b1 is complex real ext-real Element of REAL : b1 in x } is set
c5 is complex real ext-real Element of REAL
A + c5 is complex real ext-real Element of REAL
A is complex real ext-real Element of REAL
x is complex-membered ext-real-membered real-membered Element of bool REAL
(x,A) is complex-membered ext-real-membered real-membered Element of bool REAL
{A} is non empty finite complex-membered ext-real-membered real-membered left_end right_end bounded_below bounded_above real-bounded set
{A} ++ x is complex-membered ext-real-membered real-membered set
{ K430(b1,b2) where b1, b2 is complex Element of COMPLEX : ( b1 in {A} & b2 in x ) } is set
{A} ++ x is ext-real-membered set
{ (b1 + b2) where b1, b2 is ext-real Element of ExtREAL : ( b1 in {A} & b2 in x ) } is set
A ++ x is ext-real-membered set
{ (A + b1) where b1 is complex real ext-real Element of REAL : b1 in x } is set
NAT --> A is Relation-like NAT -defined REAL -valued T-Sequence-like non empty Function-like constant total V30( NAT , REAL ) complex-valued ext-real-valued real-valued bounded_above bounded_below bounded convergent Element of bool [:NAT,REAL:]
a is Relation-like NAT -defined REAL -valued non empty Function-like total V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
rng a is non empty complex-membered ext-real-membered real-membered set
lim a is complex real ext-real Element of REAL
rng a is non empty complex-membered ext-real-membered real-membered Element of bool REAL
a is Relation-like NAT -defined REAL -valued non empty Function-like total V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
a - a is Relation-like NAT -defined REAL -valued non empty Function-like total V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
- a is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
- 1 is complex real ext-real non positive integer set
(- 1) * a is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
a + (- a) is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
lim (a - a) is complex real ext-real Element of REAL
a . 0 is complex real ext-real Element of ExtREAL
(lim a) - (a . 0) is complex real ext-real Element of REAL
- (a . 0) is complex real ext-real set
(lim a) + (- (a . 0)) is complex real ext-real set
(lim a) - A is complex real ext-real Element of REAL
- A is complex real ext-real set
(lim a) + (- A) is complex real ext-real set
A + (lim (a - a)) is complex real ext-real Element of REAL
rng (a - a) is non empty complex-membered ext-real-membered real-membered Element of bool REAL
c5 is set
dom (a - a) is non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end bounded_below Element of bool NAT
r3 is set
(a - a) . r3 is complex real ext-real Element of ExtREAL
n is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below integer V90() Element of NAT
a . n is complex real ext-real Element of ExtREAL
- a is Relation-like NAT -defined REAL -valued non empty Function-like total V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
(- a) . n is complex real ext-real Element of ExtREAL
(a . n) + ((- a) . n) is complex real ext-real Element of ExtREAL
(a . n) + ((- a) . n) is complex real ext-real set
a . n is complex real ext-real Element of ExtREAL
- (a . n) is complex real ext-real Element of ExtREAL
- (a . n) is complex real ext-real set
(a . n) + (- (a . n)) is complex real ext-real Element of ExtREAL
(a . n) + (- (a . n)) is complex real ext-real set
(a . n) - A is complex real ext-real Element of REAL
(a . n) + (- A) is complex real ext-real set
x1 is complex real ext-real Element of REAL
x1 + A is complex real ext-real Element of REAL
A is complex-membered ext-real-membered real-membered Element of bool REAL
x is complex real ext-real Element of REAL
(A,x) is complex-membered ext-real-membered real-membered Element of bool REAL
{x} is non empty finite complex-membered ext-real-membered real-membered left_end right_end bounded_below bounded_above real-bounded set
{x} ++ A is complex-membered ext-real-membered real-membered set
{ K430(b1,b2) where b1, b2 is complex Element of COMPLEX : ( b1 in {x} & b2 in A ) } is set
{x} ++ A is ext-real-membered set
{ (b1 + b2) where b1, b2 is ext-real Element of ExtREAL : ( b1 in {x} & b2 in A ) } is set
x ++ A is ext-real-membered set
- x is complex real ext-real Element of REAL
((A,x),(- x)) is complex-membered ext-real-membered real-membered Element of bool REAL
{(- x)} is non empty finite complex-membered ext-real-membered real-membered left_end right_end bounded_below bounded_above real-bounded set
{(- x)} ++ (A,x) is complex-membered ext-real-membered real-membered set
{ K430(b1,b2) where b1, b2 is complex Element of COMPLEX : ( b1 in {(- x)} & b2 in (A,x) ) } is set
{(- x)} ++ (A,x) is ext-real-membered set
{ (b1 + b2) where b1, b2 is ext-real Element of ExtREAL : ( b1 in {(- x)} & b2 in (A,x) ) } is set
(- x) ++ (A,x) is ext-real-membered set
(- x) + x is complex real ext-real Element of REAL
(A,((- x) + x)) is complex-membered ext-real-membered real-membered Element of bool REAL
{((- x) + x)} is non empty finite complex-membered ext-real-membered real-membered left_end right_end bounded_below bounded_above real-bounded set
{((- x) + x)} ++ A is complex-membered ext-real-membered real-membered set
{ K430(b1,b2) where b1, b2 is complex Element of COMPLEX : ( b1 in {((- x) + x)} & b2 in A ) } is set
{((- x) + x)} ++ A is ext-real-membered set
{ (b1 + b2) where b1, b2 is ext-real Element of ExtREAL : ( b1 in {((- x) + x)} & b2 in A ) } is set
((- x) + x) ++ A is ext-real-membered set
A is complex-membered ext-real-membered real-membered Element of bool REAL
{ (1 / b1) where b1 is complex real ext-real Element of REAL : b1 in A } is set
{ H1(b1) where b1 is complex real ext-real Element of REAL : S1[b1] } is set
x is complex-membered ext-real-membered real-membered Element of bool REAL
a is complex-membered ext-real-membered real-membered Element of bool REAL
{ (1 / b1) where b1 is complex real ext-real Element of REAL : b1 in a } is set
{ (1 / b1) where b1 is complex real ext-real Element of REAL : b1 in x } is set
a is set
c5 is complex real ext-real Element of REAL
1 / c5 is complex real ext-real Element of REAL
c5 " is complex real ext-real set
1 * (c5 ") is complex real ext-real set
1 / (1 / c5) is complex real ext-real Element of REAL
(1 / c5) " is complex real ext-real set
1 * ((1 / c5) ") is complex real ext-real set
a is set
c5 is complex real ext-real Element of REAL
1 / c5 is complex real ext-real Element of REAL
c5 " is complex real ext-real set
1 * (c5 ") is complex real ext-real set
r3 is complex real ext-real Element of REAL
1 / r3 is complex real ext-real Element of REAL
r3 " is complex real ext-real set
1 * (r3 ") is complex real ext-real set
A is complex real ext-real set
1 / A is complex real ext-real Element of REAL
A " is complex real ext-real set
1 * (A ") is complex real ext-real set
x is complex-membered ext-real-membered real-membered Element of bool REAL
(x) is complex-membered ext-real-membered real-membered Element of bool REAL
{ (1 / b1) where b1 is complex real ext-real Element of REAL : b1 in x } is set
a is complex real ext-real Element of REAL
1 / a is complex real ext-real Element of REAL
a " is complex real ext-real set
1 * (a ") is complex real ext-real set
A is non empty complex-membered ext-real-membered real-membered Element of bool REAL
(A) is complex-membered ext-real-membered real-membered Element of bool REAL
{ (1 / b1) where b1 is complex real ext-real Element of REAL : b1 in A } is set
x is complex real ext-real Element of REAL
A is complex-membered ext-real-membered real-membered with_non-empty_elements Element of bool REAL
(A) is complex-membered ext-real-membered real-membered Element of bool REAL
{ (1 / b1) where b1 is complex real ext-real Element of REAL : b1 in A } is set
x is complex real ext-real Element of REAL
1 / x is complex real ext-real Element of REAL
x " is complex real ext-real set
1 * (x ") is complex real ext-real set
A is complex-membered ext-real-membered real-membered with_non-empty_elements Element of bool REAL
(A) is complex-membered ext-real-membered real-membered with_non-empty_elements Element of bool REAL
{ (1 / b1) where b1 is complex real ext-real Element of REAL : b1 in A } is set
x is Relation-like NAT -defined REAL -valued non empty Function-like total V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
rng x is non empty complex-membered ext-real-membered real-membered set
lim x is complex real ext-real Element of REAL
rng x is non empty complex-membered ext-real-membered real-membered Element of bool REAL
x " is Relation-like NAT -defined REAL -valued non empty Function-like total V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
rng (x ") is non empty complex-membered ext-real-membered real-membered Element of bool REAL
a is set
dom (x ") is non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end bounded_below Element of bool NAT
a is set
(x ") . a is complex real ext-real Element of ExtREAL
c5 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below integer V90() Element of NAT
x . c5 is complex real ext-real Element of ExtREAL
1 / (x . c5) is complex real ext-real Element of REAL
(x . c5) " is complex real ext-real set
1 * ((x . c5) ") is complex real ext-real set
((A)) is complex-membered ext-real-membered real-membered with_non-empty_elements Element of bool REAL
{ (1 / b1) where b1 is complex real ext-real Element of REAL : b1 in (A) } is set
a is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below integer V90() Element of NAT
x . a is complex real ext-real Element of ExtREAL
a is set
dom (x ") is non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end bounded_below Element of bool NAT
a is set
(x ") . a is complex real ext-real Element of ExtREAL
c5 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below integer V90() Element of NAT
x . c5 is complex real ext-real Element of ExtREAL
1 / (x . c5) is complex real ext-real Element of REAL
(x . c5) " is complex real ext-real set
1 * ((x . c5) ") is complex real ext-real set
((A)) is complex-membered ext-real-membered real-membered with_non-empty_elements Element of bool REAL
{ (1 / b1) where b1 is complex real ext-real Element of REAL : b1 in (A) } is set
lim (x ") is complex real ext-real Element of REAL
1 / (lim x) is complex real ext-real Element of REAL
(lim x) " is complex real ext-real set
1 * ((lim x) ") is complex real ext-real set
1 / (1 / (lim x)) is complex real ext-real Element of REAL
(1 / (lim x)) " is complex real ext-real set
1 * ((1 / (lim x)) ") is complex real ext-real set
A is Element of bool (bool REAL)
meet A is complex-membered ext-real-membered real-membered Element of bool REAL
x is Relation-like NAT -defined REAL -valued non empty Function-like total V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
rng x is non empty complex-membered ext-real-membered real-membered set
lim x is complex real ext-real Element of REAL
rng x is non empty complex-membered ext-real-membered real-membered Element of bool REAL
a is set
r3 is set
c5 is complex-membered ext-real-membered real-membered Element of bool REAL
A is complex-membered ext-real-membered real-membered Element of bool REAL
{ b1 where b1 is complex-membered ext-real-membered real-membered Element of bool REAL : ( A c= b1 & b1 is closed ) } is set
meet { b1 where b1 is complex-membered ext-real-membered real-membered Element of bool REAL : ( A c= b1 & b1 is closed ) } is set
{ b1 where b1 is complex-membered ext-real-membered real-membered Element of bool REAL : S1[b1] } is set
x is Element of bool (bool REAL)
a is Element of bool (bool REAL)
meet a is complex-membered ext-real-membered real-membered Element of bool REAL
[#] REAL is non empty non proper complex-membered ext-real-membered real-membered closed open Element of bool REAL
a is complex-membered ext-real-membered real-membered Element of bool REAL
a is complex-membered ext-real-membered real-membered Element of bool REAL
{ b1 where b1 is complex-membered ext-real-membered real-membered Element of bool REAL : ( a c= b1 & b1 is closed ) } is set
meet { b1 where b1 is complex-membered ext-real-membered real-membered Element of bool REAL : ( a c= b1 & b1 is closed ) } is set
{ b1 where b1 is complex-membered ext-real-membered real-membered Element of bool REAL : ( a c= b1 & b1 is closed ) } is set
meet { b1 where b1 is complex-membered ext-real-membered real-membered Element of bool REAL : ( a c= b1 & b1 is closed ) } is set
x is complex-membered ext-real-membered real-membered Element of bool REAL
x1 is set
n is set
m is complex-membered ext-real-membered real-membered Element of bool REAL
m1 is set
oi is complex-membered ext-real-membered real-membered Element of bool REAL
x1 is set
n is set
m is complex-membered ext-real-membered real-membered Element of bool REAL
A is complex-membered ext-real-membered real-membered Element of bool REAL
(A) is complex-membered ext-real-membered real-membered Element of bool REAL
{ b1 where b1 is complex-membered ext-real-membered real-membered Element of bool REAL : ( A c= b1 & b1 is closed ) } is set
meet { b1 where b1 is complex-membered ext-real-membered real-membered Element of bool REAL : ( A c= b1 & b1 is closed ) } is set
{ b1 where b1 is complex-membered ext-real-membered real-membered Element of bool REAL : S1[b1] } is set
x is Element of bool (bool REAL)
a is Element of bool (bool REAL)
a is complex-membered ext-real-membered real-membered Element of bool REAL
c5 is complex-membered ext-real-membered real-membered Element of bool REAL
A is complex-membered ext-real-membered real-membered Element of bool REAL
(A) is complex-membered ext-real-membered real-membered closed Element of bool REAL
{ b1 where b1 is complex-membered ext-real-membered real-membered Element of bool REAL : ( A c= b1 & b1 is closed ) } is set
meet { b1 where b1 is complex-membered ext-real-membered real-membered Element of bool REAL : ( A c= b1 & b1 is closed ) } is set
x is complex-membered ext-real-membered real-membered closed Element of bool REAL
A is complex-membered ext-real-membered real-membered Element of bool REAL
(A) is complex-membered ext-real-membered real-membered closed Element of bool REAL
{ b1 where b1 is complex-membered ext-real-membered real-membered Element of bool REAL : ( A c= b1 & b1 is closed ) } is set
meet { b1 where b1 is complex-membered ext-real-membered real-membered Element of bool REAL : ( A c= b1 & b1 is closed ) } is set
x is set
a is set
c5 is complex-membered ext-real-membered real-membered Element of bool REAL
[#] REAL is non empty non proper complex-membered ext-real-membered real-membered closed open Element of bool REAL
A is complex-membered ext-real-membered real-membered Element of bool REAL
(A) is complex-membered ext-real-membered real-membered closed Element of bool REAL
{ b1 where b1 is complex-membered ext-real-membered real-membered Element of bool REAL : ( A c= b1 & b1 is closed ) } is set
meet { b1 where b1 is complex-membered ext-real-membered real-membered Element of bool REAL : ( A c= b1 & b1 is closed ) } is set
{} REAL is Relation-like non-zero empty-yielding RAT -valued epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural empty proper complex real ext-real non positive non negative finite finite-yielding V37() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V47() complex-valued ext-real-valued real-valued natural-valued bounded_below bounded_above real-bounded interval open_interval closed open integer Element of bool REAL
(({} REAL)) is complex-membered ext-real-membered real-membered closed Element of bool REAL
{ b1 where b1 is complex-membered ext-real-membered real-membered Element of bool REAL : ( {} REAL c= b1 & b1 is closed ) } is set
meet { b1 where b1 is complex-membered ext-real-membered real-membered Element of bool REAL : ( {} REAL c= b1 & b1 is closed ) } is set
[#] REAL is non empty non proper complex-membered ext-real-membered real-membered closed open Element of bool REAL
(([#] REAL)) is complex-membered ext-real-membered real-membered closed Element of bool REAL
{ b1 where b1 is complex-membered ext-real-membered real-membered Element of bool REAL : ( [#] REAL c= b1 & b1 is closed ) } is set
meet { b1 where b1 is complex-membered ext-real-membered real-membered Element of bool REAL : ( [#] REAL c= b1 & b1 is closed ) } is set
A is complex-membered ext-real-membered real-membered Element of bool REAL
(A) is complex-membered ext-real-membered real-membered closed Element of bool REAL
{ b1 where b1 is complex-membered ext-real-membered real-membered Element of bool REAL : ( A c= b1 & b1 is closed ) } is set
meet { b1 where b1 is complex-membered ext-real-membered real-membered Element of bool REAL : ( A c= b1 & b1 is closed ) } is set
x is complex-membered ext-real-membered real-membered Element of bool REAL
(x) is complex-membered ext-real-membered real-membered closed Element of bool REAL
{ b1 where b1 is complex-membered ext-real-membered real-membered Element of bool REAL : ( x c= b1 & b1 is closed ) } is set
meet { b1 where b1 is complex-membered ext-real-membered real-membered Element of bool REAL : ( x c= b1 & b1 is closed ) } is set
A is complex-membered ext-real-membered real-membered Element of bool REAL
(A) is complex-membered ext-real-membered real-membered closed Element of bool REAL
{ b1 where b1 is complex-membered ext-real-membered real-membered Element of bool REAL : ( A c= b1 & b1 is closed ) } is set
meet { b1 where b1 is complex-membered ext-real-membered real-membered Element of bool REAL : ( A c= b1 & b1 is closed ) } is set
x is complex real ext-real Element of REAL
a is complex-membered ext-real-membered real-membered open Element of bool REAL
a /\ A is complex-membered ext-real-membered real-membered Element of bool REAL
a ` is complex-membered ext-real-membered real-membered Element of bool REAL
REAL \ a is complex-membered ext-real-membered real-membered set
(A) ` is complex-membered ext-real-membered real-membered Element of bool REAL
REAL \ (A) is complex-membered ext-real-membered real-membered set
((A) `) ` is complex-membered ext-real-membered real-membered Element of bool REAL
REAL \ ((A) `) is complex-membered ext-real-membered real-membered set
((A) `) /\ A is complex-membered ext-real-membered real-membered Element of bool REAL
A is complex-membered ext-real-membered real-membered Element of bool REAL
(A) is complex-membered ext-real-membered real-membered closed Element of bool REAL
{ b1 where b1 is complex-membered ext-real-membered real-membered Element of bool REAL : ( A c= b1 & b1 is closed ) } is set
meet { b1 where b1 is complex-membered ext-real-membered real-membered Element of bool REAL : ( A c= b1 & b1 is closed ) } is set
x is complex real ext-real Element of REAL
a is set
a is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below integer V90() Element of NAT
a + 1 is epsilon-transitive epsilon-connected ordinal natural non empty complex real ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end bounded_below integer V90() Element of NAT
1 / (a + 1) is complex real ext-real non negative Element of REAL
(a + 1) " is non empty complex real ext-real positive non negative set
1 * ((a + 1) ") is complex real ext-real non negative set
x - (1 / (a + 1)) is complex real ext-real Element of REAL
- (1 / (a + 1)) is complex real ext-real non positive set
x + (- (1 / (a + 1))) is complex real ext-real set
x + (1 / (a + 1)) is complex real ext-real Element of REAL
].(x - (1 / (a + 1))),(x + (1 / (a + 1))).[ is complex-membered ext-real-membered real-membered non left_end non right_end interval open Element of bool REAL
{ b1 where b1 is complex real ext-real Element of REAL : ( not b1 <= x - (1 / (a + 1)) & not x + (1 / (a + 1)) <= b1 ) } is set
A /\ ].(x - (1 / (a + 1))),(x + (1 / (a + 1))).[ is complex-membered ext-real-membered real-membered Element of bool REAL
choose (A /\ ].(x - (1 / (a + 1))),(x + (1 / (a + 1))).[) is complex real ext-real Element of A /\ ].(x - (1 / (a + 1))),(x + (1 / (a + 1))).[
the Element of A /\ ].(x - (1 / (a + 1))),(x + (1 / (a + 1))).[ is complex real ext-real Element of A /\ ].(x - (1 / (a + 1))),(x + (1 / (a + 1))).[
x1 is set
n is set
a is Relation-like Function-like set
dom a is set
rng a is set
a is Relation-like NAT -defined REAL -valued non empty Function-like total V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
rng a is non empty complex-membered ext-real-membered real-membered Element of bool REAL
lim a is complex real ext-real Element of REAL
c5 is set
dom a is non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end bounded_below Element of bool NAT
r3 is set
a . r3 is complex real ext-real Element of ExtREAL
x1 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer set
x1 + 1 is epsilon-transitive epsilon-connected ordinal natural non empty complex real ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end bounded_below integer V90() Element of NAT
1 / (x1 + 1) is complex real ext-real non negative Element of REAL
(x1 + 1) " is non empty complex real ext-real positive non negative set
1 * ((x1 + 1) ") is complex real ext-real non negative set
x - (1 / (x1 + 1)) is complex real ext-real Element of REAL
- (1 / (x1 + 1)) is complex real ext-real non positive set
x + (- (1 / (x1 + 1))) is complex real ext-real set
x + (1 / (x1 + 1)) is complex real ext-real Element of REAL
].(x - (1 / (x1 + 1))),(x + (1 / (x1 + 1))).[ is complex-membered ext-real-membered real-membered non left_end non right_end interval open Element of bool REAL
{ b1 where b1 is complex real ext-real Element of REAL : ( not b1 <= x - (1 / (x1 + 1)) & not x + (1 / (x1 + 1)) <= b1 ) } is set
A /\ ].(x - (1 / (x1 + 1))),(x + (1 / (x1 + 1))).[ is complex-membered ext-real-membered real-membered Element of bool REAL
choose (A /\ ].(x - (1 / (x1 + 1))),(x + (1 / (x1 + 1))).[) is complex real ext-real Element of A /\ ].(x - (1 / (x1 + 1))),(x + (1 / (x1 + 1))).[
the Element of A /\ ].(x - (1 / (x1 + 1))),(x + (1 / (x1 + 1))).[ is complex real ext-real Element of A /\ ].(x - (1 / (x1 + 1))),(x + (1 / (x1 + 1))).[
n is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below integer V90() Element of NAT
n + 1 is epsilon-transitive epsilon-connected ordinal natural non empty complex real ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end bounded_below integer V90() Element of NAT
1 / (n + 1) is complex real ext-real non negative Element of REAL
(n + 1) " is non empty complex real ext-real positive non negative set
1 * ((n + 1) ") is complex real ext-real non negative set
x - (1 / (n + 1)) is complex real ext-real Element of REAL
- (1 / (n + 1)) is complex real ext-real non positive set
x + (- (1 / (n + 1))) is complex real ext-real set
x + (1 / (n + 1)) is complex real ext-real Element of REAL
].(x - (1 / (n + 1))),(x + (1 / (n + 1))).[ is complex-membered ext-real-membered real-membered non left_end non right_end interval open Element of bool REAL
{ b1 where b1 is complex real ext-real Element of REAL : ( not b1 <= x - (1 / (n + 1)) & not x + (1 / (n + 1)) <= b1 ) } is set
A /\ ].(x - (1 / (n + 1))),(x + (1 / (n + 1))).[ is complex-membered ext-real-membered real-membered Element of bool REAL
c5 is complex real ext-real set
1 / c5 is complex real ext-real Element of REAL
c5 " is complex real ext-real set
1 * (c5 ") is complex real ext-real set
[/(1 / c5)\] is complex real ext-real integer set
x1 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below integer V90() Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below integer V90() Element of NAT
n + 1 is epsilon-transitive epsilon-connected ordinal natural non empty complex real ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end bounded_below integer V90() Element of NAT
1 / n is complex real ext-real non negative Element of REAL
n " is complex real ext-real non negative set
1 * (n ") is complex real ext-real non negative set
1 / (n + 1) is complex real ext-real non negative Element of REAL
(n + 1) " is non empty complex real ext-real positive non negative set
1 * ((n + 1) ") is complex real ext-real non negative set
1 / x1 is complex real ext-real non negative Element of REAL
x1 " is complex real ext-real non negative set
1 * (x1 ") is complex real ext-real non negative set
1 / (1 / c5) is complex real ext-real Element of REAL
(1 / c5) " is complex real ext-real set
1 * ((1 / c5) ") is complex real ext-real set
m is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below integer V90() Element of NAT
m + 1 is epsilon-transitive epsilon-connected ordinal natural non empty complex real ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end bounded_below integer V90() Element of NAT
1 / (m + 1) is complex real ext-real non negative Element of REAL
(m + 1) " is non empty complex real ext-real positive non negative set
1 * ((m + 1) ") is complex real ext-real non negative set
x - (1 / (m + 1)) is complex real ext-real Element of REAL
- (1 / (m + 1)) is complex real ext-real non positive set
x + (- (1 / (m + 1))) is complex real ext-real set
x + (1 / (m + 1)) is complex real ext-real Element of REAL
].(x - (1 / (m + 1))),(x + (1 / (m + 1))).[ is complex-membered ext-real-membered real-membered non left_end non right_end interval open Element of bool REAL
{ b1 where b1 is complex real ext-real Element of REAL : ( not b1 <= x - (1 / (m + 1)) & not x + (1 / (m + 1)) <= b1 ) } is set
A /\ ].(x - (1 / (m + 1))),(x + (1 / (m + 1))).[ is complex-membered ext-real-membered real-membered Element of bool REAL
a . m is complex real ext-real Element of ExtREAL
s is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer set
s + 1 is epsilon-transitive epsilon-connected ordinal natural non empty complex real ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end bounded_below integer V90() Element of NAT
1 / (s + 1) is complex real ext-real non negative Element of REAL
(s + 1) " is non empty complex real ext-real positive non negative set
1 * ((s + 1) ") is complex real ext-real non negative set
x - (1 / (s + 1)) is complex real ext-real Element of REAL
- (1 / (s + 1)) is complex real ext-real non positive set
x + (- (1 / (s + 1))) is complex real ext-real set
x + (1 / (s + 1)) is complex real ext-real Element of REAL
].(x - (1 / (s + 1))),(x + (1 / (s + 1))).[ is complex-membered ext-real-membered real-membered non left_end non right_end interval open Element of bool REAL
{ b1 where b1 is complex real ext-real Element of REAL : ( not b1 <= x - (1 / (s + 1)) & not x + (1 / (s + 1)) <= b1 ) } is set
A /\ ].(x - (1 / (s + 1))),(x + (1 / (s + 1))).[ is complex-membered ext-real-membered real-membered Element of bool REAL
choose (A /\ ].(x - (1 / (s + 1))),(x + (1 / (s + 1))).[) is complex real ext-real Element of A /\ ].(x - (1 / (s + 1))),(x + (1 / (s + 1))).[
the Element of A /\ ].(x - (1 / (s + 1))),(x + (1 / (s + 1))).[ is complex real ext-real Element of A /\ ].(x - (1 / (s + 1))),(x + (1 / (s + 1))).[
s is complex real ext-real Element of REAL
s - x is complex real ext-real Element of REAL
- x is complex real ext-real set
s + (- x) is complex real ext-real set
- (1 / (m + 1)) is complex real ext-real non positive Element of REAL
abs (s - x) is complex real ext-real Element of REAL
(a . m) - x is complex real ext-real Element of REAL
(a . m) + (- x) is complex real ext-real set
abs ((a . m) - x) is complex real ext-real Element of REAL
A is set
[:A,REAL:] is Relation-like complex-valued ext-real-valued real-valued set
bool [:A,REAL:] is non empty set
x is Relation-like A -defined REAL -valued Function-like total V30(A, REAL ) complex-valued ext-real-valued real-valued Element of bool [:A,REAL:]
x .: A is complex-membered ext-real-membered real-membered Element of bool REAL
dom x is Element of bool A
bool A is non empty set
a is complex real ext-real set
a is ext-real set
c5 is set
x . c5 is complex real ext-real Element of ExtREAL
a is complex real ext-real set
a - 1 is complex real ext-real Element of REAL
- 1 is complex real ext-real non positive integer set
a + (- 1) is complex real ext-real set
dom x is set
a is set
x . a is complex real ext-real Element of REAL
x . a is complex real ext-real Element of ExtREAL
rng x is complex-membered ext-real-membered real-membered Element of bool REAL
(x . a) + 1 is complex real ext-real Element of REAL
dom x is Element of bool A
bool A is non empty set
a is complex real ext-real set
a is ext-real set
c5 is set
x . c5 is complex real ext-real Element of ExtREAL
a is complex real ext-real set
a + 1 is complex real ext-real Element of REAL
dom x is set
a is set
x . a is complex real ext-real Element of REAL
x . a is complex real ext-real Element of ExtREAL
rng x is complex-membered ext-real-membered real-membered Element of bool REAL
(x . a) + 1 is complex real ext-real Element of REAL
A is set
[:A,REAL:] is Relation-like complex-valued ext-real-valued real-valued set
bool [:A,REAL:] is non empty set
A is set
[:A,REAL:] is Relation-like complex-valued ext-real-valued real-valued set
bool [:A,REAL:] is non empty set
x is set
a is Relation-like A -defined REAL -valued Function-like total V30(A, REAL ) complex-valued ext-real-valued real-valued Element of bool [:A,REAL:]
- a is Relation-like A -defined REAL -valued Function-like total V30(A, REAL ) complex-valued ext-real-valued real-valued Element of bool [:A,REAL:]
- 1 is complex real ext-real non positive integer set
(- 1) * a is Relation-like A -defined Function-like total complex-valued ext-real-valued real-valued set
(- a) .: x is complex-membered ext-real-membered real-membered Element of bool REAL
a .: x is complex-membered ext-real-membered real-membered Element of bool REAL
((a .: x)) is complex-membered ext-real-membered real-membered Element of bool REAL
{ K428(b1) where b1 is complex Element of COMPLEX : b1 in a .: x } is set
-- (a .: x) is ext-real-membered set
{ (- b1) where b1 is ext-real Element of ExtREAL : b1 in a .: x } is set
a is set
c5 is set
(- a) . c5 is complex real ext-real Element of ExtREAL
a . c5 is complex real ext-real Element of ExtREAL
- (a . c5) is complex real ext-real Element of ExtREAL
- (a . c5) is complex real ext-real set
c5 is complex Element of COMPLEX
- c5 is complex set
r3 is complex real ext-real Element of REAL
x1 is set
a . x1 is complex real ext-real Element of ExtREAL
(- a) . x1 is complex real ext-real Element of ExtREAL
A is non empty set
[:A,REAL:] is Relation-like non empty complex-valued ext-real-valued real-valued set
bool [:A,REAL:] is non empty set
x is Relation-like A -defined REAL -valued non empty Function-like total V30(A, REAL ) complex-valued ext-real-valued real-valued Element of bool [:A,REAL:]
- x is Relation-like A -defined REAL -valued non empty Function-like total V30(A, REAL ) complex-valued ext-real-valued real-valued Element of bool [:A,REAL:]
- 1 is complex real ext-real non positive integer set
(- 1) * x is Relation-like A -defined Function-like total complex-valued ext-real-valued real-valued set
x .: A is non empty complex-membered ext-real-membered real-membered Element of bool REAL
upper_bound (x .: A) is complex real ext-real Element of REAL
((x .: A)) is non empty complex-membered ext-real-membered real-membered Element of bool REAL
{ K428(b1) where b1 is complex Element of COMPLEX : b1 in x .: A } is set
-- (x .: A) is non empty ext-real-membered set
{ (- b1) where b1 is ext-real Element of ExtREAL : b1 in x .: A } is set
(- x) .: A is non empty complex-membered ext-real-membered real-membered Element of bool REAL
lower_bound ((- x) .: A) is complex real ext-real set
lower_bound ((- x) .: A) is complex real ext-real Element of REAL
(((x .: A))) is non empty complex-membered ext-real-membered real-membered Element of bool REAL
{ K428(b1) where b1 is complex Element of COMPLEX : b1 in ((x .: A)) } is set
-- ((x .: A)) is non empty ext-real-membered set
{ (- b1) where b1 is ext-real Element of ExtREAL : b1 in ((x .: A)) } is set
upper_bound (((x .: A))) is complex real ext-real Element of REAL
- (upper_bound (((x .: A)))) is complex real ext-real Element of REAL
- (upper_bound (x .: A)) is complex real ext-real Element of REAL
A is non empty set
[:A,REAL:] is Relation-like non empty complex-valued ext-real-valued real-valued set
bool [:A,REAL:] is non empty set
x is Relation-like A -defined REAL -valued non empty Function-like total V30(A, REAL ) complex-valued ext-real-valued real-valued Element of bool [:A,REAL:]
- x is Relation-like A -defined REAL -valued non empty Function-like total V30(A, REAL ) complex-valued ext-real-valued real-valued Element of bool [:A,REAL:]
- 1 is complex real ext-real non positive integer set
(- 1) * x is Relation-like A -defined Function-like total complex-valued ext-real-valued real-valued set
x .: A is non empty complex-membered ext-real-membered real-membered Element of bool REAL
lower_bound (x .: A) is complex real ext-real Element of REAL
((x .: A)) is non empty complex-membered ext-real-membered real-membered Element of bool REAL
{ K428(b1) where b1 is complex Element of COMPLEX : b1 in x .: A } is set
-- (x .: A) is non empty ext-real-membered set
{ (- b1) where b1 is ext-real Element of ExtREAL : b1 in x .: A } is set
(- x) .: A is non empty complex-membered ext-real-membered real-membered Element of bool REAL
upper_bound ((- x) .: A) is complex real ext-real set
upper_bound ((- x) .: A) is complex real ext-real Element of REAL
(((x .: A))) is non empty complex-membered ext-real-membered real-membered Element of bool REAL
{ K428(b1) where b1 is complex Element of COMPLEX : b1 in ((x .: A)) } is set
-- ((x .: A)) is non empty ext-real-membered set
{ (- b1) where b1 is ext-real Element of ExtREAL : b1 in ((x .: A)) } is set
lower_bound (((x .: A))) is complex real ext-real Element of REAL
- (lower_bound (((x .: A)))) is complex real ext-real Element of REAL
- (lower_bound (x .: A)) is complex real ext-real Element of REAL
A is non empty set
[:A,REAL:] is Relation-like non empty complex-valued ext-real-valued real-valued set
bool [:A,REAL:] is non empty set
x is Relation-like A -defined REAL -valued non empty Function-like total V30(A, REAL ) complex-valued ext-real-valued real-valued Element of bool [:A,REAL:]
- x is Relation-like A -defined REAL -valued non empty Function-like total V30(A, REAL ) complex-valued ext-real-valued real-valued Element of bool [:A,REAL:]
- 1 is complex real ext-real non positive integer set
(- 1) * x is Relation-like A -defined Function-like total complex-valued ext-real-valued real-valued set
- (- x) is Relation-like A -defined REAL -valued non empty Function-like total V30(A, REAL ) complex-valued ext-real-valued real-valued Element of bool [:A,REAL:]
(- 1) * (- x) is Relation-like A -defined Function-like total complex-valued ext-real-valued real-valued set
A is non empty set
[:A,REAL:] is Relation-like non empty complex-valued ext-real-valued real-valued set
bool [:A,REAL:] is non empty set
x is Relation-like A -defined REAL -valued non empty Function-like total V30(A, REAL ) complex-valued ext-real-valued real-valued Element of bool [:A,REAL:]
- x is Relation-like A -defined REAL -valued non empty Function-like total V30(A, REAL ) complex-valued ext-real-valued real-valued Element of bool [:A,REAL:]
- 1 is complex real ext-real non positive integer set
(- 1) * x is Relation-like A -defined Function-like total complex-valued ext-real-valued real-valued set
- (- x) is Relation-like A -defined REAL -valued non empty Function-like total V30(A, REAL ) complex-valued ext-real-valued real-valued Element of bool [:A,REAL:]
(- 1) * (- x) is Relation-like A -defined Function-like total complex-valued ext-real-valued real-valued set
A is set
[:A,REAL:] is Relation-like complex-valued ext-real-valued real-valued set
bool [:A,REAL:] is non empty set
x is complex-membered ext-real-membered real-membered Element of bool REAL
(x) is complex-membered ext-real-membered real-membered Element of bool REAL
{ K428(b1) where b1 is complex Element of COMPLEX : b1 in x } is set
-- x is ext-real-membered set
{ (- b1) where b1 is ext-real Element of ExtREAL : b1 in x } is set
a is Relation-like A -defined REAL -valued Function-like total V30(A, REAL ) complex-valued ext-real-valued real-valued Element of bool [:A,REAL:]
- a is Relation-like A -defined REAL -valued Function-like total V30(A, REAL ) complex-valued ext-real-valued real-valued Element of bool [:A,REAL:]
- 1 is complex real ext-real non positive integer set
(- 1) * a is Relation-like A -defined Function-like total complex-valued ext-real-valued real-valued set
(- a) " x is Element of bool A
bool A is non empty set
a " (x) is Element of bool A
a is set
(- a) . a is complex real ext-real Element of ExtREAL
a . a is complex real ext-real Element of ExtREAL
- (a . a) is complex real ext-real Element of ExtREAL
- (a . a) is complex real ext-real set
- (- (a . a)) is complex real ext-real Element of ExtREAL
- (- (a . a)) is complex real ext-real set
((x)) is complex-membered ext-real-membered real-membered Element of bool REAL
{ K428(b1) where b1 is complex Element of COMPLEX : b1 in (x) } is set
-- (x) is ext-real-membered set
{ (- b1) where b1 is ext-real Element of ExtREAL : b1 in (x) } is set
A is set
[:A,REAL:] is Relation-like complex-valued ext-real-valued real-valued set
bool [:A,REAL:] is non empty set
x is set
a is Relation-like A -defined REAL -valued Function-like total V30(A, REAL ) complex-valued ext-real-valued real-valued Element of bool [:A,REAL:]
a .: x is complex-membered ext-real-membered real-membered Element of bool REAL
a is complex real ext-real Element of REAL
a + a is Relation-like A -defined REAL -valued Function-like total V30(A, REAL ) complex-valued ext-real-valued real-valued Element of bool [:A,REAL:]
(a + a) .: x is complex-membered ext-real-membered real-membered Element of bool REAL
((a .: x),a) is complex-membered ext-real-membered real-membered Element of bool REAL
{a} is non empty finite complex-membered ext-real-membered real-membered left_end right_end bounded_below bounded_above real-bounded set
{a} ++ (a .: x) is complex-membered ext-real-membered real-membered set
{ K430(b1,b2) where b1, b2 is complex Element of COMPLEX : ( b1 in {a} & b2 in a .: x ) } is set
{a} ++ (a .: x) is ext-real-membered set
{ (b1 + b2) where b1, b2 is ext-real Element of ExtREAL : ( b1 in {a} & b2 in a .: x ) } is set
a ++ (a .: x) is ext-real-membered set
c5 is set
r3 is set
(a + a) . r3 is complex real ext-real Element of ExtREAL
a . r3 is complex real ext-real Element of ExtREAL
a + (a . r3) is complex real ext-real Element of REAL
{ (a + b1) where b1 is complex real ext-real Element of REAL : b1 in a .: x } is set
r3 is complex real ext-real Element of REAL
a + r3 is complex real ext-real Element of REAL
x1 is set
a . x1 is complex real ext-real Element of ExtREAL
(a + a) . x1 is complex real ext-real Element of ExtREAL
A is set
[:A,REAL:] is Relation-like complex-valued ext-real-valued real-valued set
bool [:A,REAL:] is non empty set
x is complex-membered ext-real-membered real-membered Element of bool REAL
a is Relation-like A -defined REAL -valued Function-like total V30(A, REAL ) complex-valued ext-real-valued real-valued Element of bool [:A,REAL:]
a is complex real ext-real Element of REAL
a + a is Relation-like A -defined REAL -valued Function-like total V30(A, REAL ) complex-valued ext-real-valued real-valued Element of bool [:A,REAL:]
(a + a) " x is Element of bool A
bool A is non empty set
- a is complex real ext-real Element of REAL
(x,(- a)) is complex-membered ext-real-membered real-membered Element of bool REAL
{(- a)} is non empty finite complex-membered ext-real-membered real-membered left_end right_end bounded_below bounded_above real-bounded set
{(- a)} ++ x is complex-membered ext-real-membered real-membered set
{ K430(b1,b2) where b1, b2 is complex Element of COMPLEX : ( b1 in {(- a)} & b2 in x ) } is set
{(- a)} ++ x is ext-real-membered set
{ (b1 + b2) where b1, b2 is ext-real Element of ExtREAL : ( b1 in {(- a)} & b2 in x ) } is set
(- a) ++ x is ext-real-membered set
a " (x,(- a)) is Element of bool A
c5 is set
(a + a) . c5 is complex real ext-real Element of ExtREAL
a . c5 is complex real ext-real Element of ExtREAL
a + (a . c5) is complex real ext-real Element of REAL
(- a) + (a + (a . c5)) is complex real ext-real Element of REAL
{ ((- a) + b1) where b1 is complex real ext-real Element of REAL : b1 in x } is set
{ (a + b1) where b1 is complex real ext-real Element of REAL : b1 in (x,(- a)) } is set
((x,(- a)),a) is complex-membered ext-real-membered real-membered Element of bool REAL
{a} is non empty finite complex-membered ext-real-membered real-membered left_end right_end bounded_below bounded_above real-bounded set
{a} ++ (x,(- a)) is complex-membered ext-real-membered real-membered set
{ K430(b1,b2) where b1, b2 is complex Element of COMPLEX : ( b1 in {a} & b2 in (x,(- a)) ) } is set
{a} ++ (x,(- a)) is ext-real-membered set
{ (b1 + b2) where b1, b2 is ext-real Element of ExtREAL : ( b1 in {a} & b2 in (x,(- a)) ) } is set
a ++ (x,(- a)) is ext-real-membered set
a + (- a) is complex real ext-real Element of REAL
(x,(a + (- a))) is complex-membered ext-real-membered real-membered Element of bool REAL
{(a + (- a))} is non empty finite complex-membered ext-real-membered real-membered left_end right_end bounded_below bounded_above real-bounded set
{(a + (- a))} ++ x is complex-membered ext-real-membered real-membered set
{ K430(b1,b2) where b1, b2 is complex Element of COMPLEX : ( b1 in {(a + (- a))} & b2 in x ) } is set
{(a + (- a))} ++ x is ext-real-membered set
{ (b1 + b2) where b1, b2 is ext-real Element of ExtREAL : ( b1 in {(a + (- a))} & b2 in x ) } is set
(a + (- a)) ++ x is ext-real-membered set
A is set
x is complex-membered ext-real-membered real-membered set
[:A,x:] is Relation-like complex-valued ext-real-valued real-valued set
bool [:A,x:] is non empty set
a is Relation-like A -defined x -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:A,x:]
a " is Relation-like A -defined Function-like complex-valued ext-real-valued real-valued set
[:A,REAL:] is Relation-like complex-valued ext-real-valued real-valued set
bool [:A,REAL:] is non empty set
a " is Relation-like A -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:A,REAL:]
A is set
[:A,REAL:] is Relation-like complex-valued ext-real-valued real-valued set
bool [:A,REAL:] is non empty set
x is complex-membered ext-real-membered real-membered with_non-empty_elements Element of bool REAL
(x) is complex-membered ext-real-membered real-membered with_non-empty_elements Element of bool REAL
{ (1 / b1) where b1 is complex real ext-real Element of REAL : b1 in x } is set
a is Relation-like A -defined REAL -valued Function-like total V30(A, REAL ) complex-valued ext-real-valued real-valued Element of bool [:A,REAL:]
(A,REAL,a) is Relation-like A -defined REAL -valued Function-like total V30(A, REAL ) complex-valued ext-real-valued real-valued Element of bool [:A,REAL:]
(A,REAL,a) " x is Element of bool A
bool A is non empty set
a " (x) is Element of bool A
a is set
(A,REAL,a) . a is complex real ext-real Element of ExtREAL
a . a is complex real ext-real Element of ExtREAL
(a . a) " is complex real ext-real set
1 / ((a . a) ") is complex real ext-real Element of REAL
((a . a) ") " is complex real ext-real set
1 * (((a . a) ") ") is complex real ext-real set
1 / (a . a) is complex real ext-real Element of REAL
1 * ((a . a) ") is complex real ext-real set
((x)) is complex-membered ext-real-membered real-membered with_non-empty_elements Element of bool REAL
{ (1 / b1) where b1 is complex real ext-real Element of REAL : b1 in (x) } is set
A is complex-membered ext-real-membered real-membered Element of bool REAL
(A) is complex-membered ext-real-membered real-membered Element of bool REAL
{ K428(b1) where b1 is complex Element of COMPLEX : b1 in A } is set
-- A is ext-real-membered set
{ (- b1) where b1 is ext-real Element of ExtREAL : b1 in A } is set
x is complex real ext-real Element of REAL
{ (- b1) where b1 is complex Element of COMPLEX : b1 in A } is set
a is complex Element of COMPLEX
- a is complex set
a is complex real ext-real Element of REAL
- a is complex real ext-real Element of REAL