:: MEASURE6 semantic presentation

bool REAL is non empty set

bool is non empty set
bool ExtREAL is non empty set

bool omega is non empty set
COMPLEX is non empty non trivial non finite complex-membered V47() non empty-membered set

bool NAT is non empty set

bool is non empty set

bool is non empty set

bool is non empty set

bool is non empty set

bool is non empty set

bool is non empty set

bool is non empty set

bool is non empty set

bool is non empty set

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

bool is non empty set

bool is non empty set

dom A is set
rng A is set

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

rng (Ser A) is non empty ext-real-membered V67() Element of bool ExtREAL
sup (rng (Ser A)) is ext-real Element of ExtREAL

A . a is ext-real Element of ExtREAL

A . a is ext-real Element of ExtREAL
(Ser A) . a is ext-real Element of ExtREAL

(Ser A) . c5 is ext-real Element of ExtREAL

A . (c5 + 1) is ext-real Element of ExtREAL
((Ser A) . c5) + (A . (c5 + 1)) is ext-real Element of ExtREAL

A is ext-real set

r3 is ext-real Element of ExtREAL
r3 / 2 is ext-real 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

n / 2 is ext-real set
n * (2 ") is ext-real set

c5 . 0 is ext-real Element of 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

c5 . r3 is ext-real Element of ExtREAL

c5 . (r3 + 1) is ext-real Element of ExtREAL
(c5 . r3) / 2 is ext-real set

2 " is non empty complex real ext-real positive non negative set
(c5 . r3) * (2 ") is ext-real set

c5 . r3 is ext-real Element of ExtREAL
r3 is ext-real set

x1 is set
(Ser c5) . x1 is ext-real Element of ExtREAL

(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

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

(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

x is non empty ext-real-membered Element of bool 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 + (- 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

x is non empty ext-real-membered Element of bool 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 + (- 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

rng (Ser A) is non empty ext-real-membered V67() Element of bool ExtREAL
sup (rng (Ser A)) is ext-real Element of ExtREAL

A . x is ext-real Element of ExtREAL

A . a is ext-real Element of ExtREAL
(Ser A) . a is ext-real Element of ExtREAL

A . (a + 1) is ext-real Element of ExtREAL
(Ser A) . (a + 1) is ext-real Element of ExtREAL

a + (A . (a + 1)) is ext-real Element of ExtREAL

(Ser A) . 0 is ext-real Element of ExtREAL
(Ser A) . x is ext-real Element of ExtREAL

{ b1 where b1 is complex real ext-real Element of REAL : ( not b1 <= x & not a <= b1 ) } is set

{ b1 where b1 is complex real ext-real Element of REAL : ( not b1 <= a & not x <= b1 ) } is set

{ b1 where b1 is complex real ext-real Element of REAL : ( not b1 <= inf A & not sup A <= b1 ) } is set

{ b1 where b1 is complex real ext-real Element of REAL : ( not b1 <= x & not a <= b1 ) } is set

[.(inf A),(sup A).] is ext-real-membered interval set

{ b1 where b1 is complex real ext-real Element of REAL : ( x <= b1 & b1 <= a ) } is set

[.(inf A),(sup A).[ is ext-real-membered non right_end interval set

{ b1 where b1 is complex real ext-real Element of REAL : ( x <= b1 & not a <= b1 ) } is set

].(inf A),(sup A).] is ext-real-membered non left_end interval set

{ 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 ext-real Element of ExtREAL

{ K430(b1,b2) where b1, b2 is complex Element of COMPLEX : ( b1 in x & b2 in A ) } is set

{ (b1 + b2) where b1, b2 is ext-real Element of ExtREAL : ( b1 in x & b2 in A ) } is set

c5 is complex Element of COMPLEX
a + c5 is set

{ K430(b1,b2) where b1, b2 is complex Element of COMPLEX : ( b1 in {x} & b2 in A ) } is set

{ (b1 + b2) where b1, b2 is ext-real Element of ExtREAL : ( b1 in {x} & b2 in A ) } is set

{ K430(b1,b2) where b1, b2 is complex Element of COMPLEX : ( b1 in {x} & b2 in A ) } is set

{ (b1 + b2) where b1, b2 is ext-real Element of ExtREAL : ( b1 in {x} & b2 in A ) } is set

x + a is set

{ K430(b1,b2) where b1, b2 is complex Element of COMPLEX : ( b1 in {x} & b2 in A ) } is set

{ (b1 + b2) where b1, b2 is ext-real Element of ExtREAL : ( b1 in {x} & b2 in A ) } is set

((A,x),(- x)) is complex-membered ext-real-membered real-membered Element of bool REAL

{ 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

(- x) + c5 is complex real ext-real Element of REAL

a is 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 + (- x) is complex real ext-real set

(- x) + c5 is complex real ext-real Element of REAL

{ K430(b1,b2) where b1, b2 is complex Element of COMPLEX : ( b1 in {A} & b2 in x ) } is set

{ (b1 + b2) where b1, b2 is ext-real Element of ExtREAL : ( b1 in {A} & b2 in x ) } is set

a is set

a + (- A) is complex real ext-real set

{ K430(b1,b2) where b1, b2 is complex Element of COMPLEX : ( b1 in {A} & b2 in {} ) } is set

{ (b1 + b2) where b1, b2 is ext-real Element of ExtREAL : ( b1 in {A} & b2 in {} ) } is set

{ K430(b1,b2) where b1, b2 is complex Element of COMPLEX : ( b1 in {x} & b2 in A ) } is set

{ (b1 + b2) where b1, b2 is ext-real Element of ExtREAL : ( b1 in {x} & b2 in A ) } is set

{ K430(b1,b2) where b1, b2 is complex Element of COMPLEX : ( b1 in {c5} & b2 in a ) } is set

{ (b1 + b2) where b1, b2 is ext-real Element of ExtREAL : ( b1 in {c5} & b2 in a ) } is set

{ 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

{ K430(b1,b2) where b1, b2 is complex Element of COMPLEX : ( b1 in {r3} & b2 in a ) } is set

{ (b1 + b2) where b1, b2 is ext-real Element of ExtREAL : ( b1 in {r3} & b2 in a ) } is set

m1 is ext-real Element of ExtREAL
oi is ext-real Element of ExtREAL

{ b1 where b1 is complex real ext-real Element of REAL : ( not b1 <= m1 & not oi <= b1 ) } is set
s is set

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

{ K430(b1,b2) where b1, b2 is complex Element of COMPLEX : ( b1 in {a} & b2 in a ) } is set

{ (b1 + b2) where b1, b2 is ext-real Element of ExtREAL : ( b1 in {a} & b2 in a ) } is set

{ K430(b1,b2) where b1, b2 is complex Element of COMPLEX : ( b1 in {x} & b2 in A ) } is set

{ (b1 + b2) where b1, b2 is ext-real Element of ExtREAL : ( b1 in {x} & b2 in A ) } is set

{ K430(b1,b2) where b1, b2 is complex Element of COMPLEX : ( b1 in {a} & b2 in a ) } is set

{ (b1 + b2) where b1, b2 is ext-real Element of ExtREAL : ( b1 in {a} & b2 in a ) } is set

{ b1 where b1 is complex real ext-real Element of REAL : ( x1 <= b1 & b1 <= n ) } is set
r3 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

{ K430(b1,b2) where b1, b2 is complex Element of COMPLEX : ( b1 in {c5} & b2 in a ) } is set

{ (b1 + b2) where b1, b2 is ext-real Element of ExtREAL : ( b1 in {c5} & b2 in a ) } is set

oi is ext-real Element of ExtREAL

c is set

c5 + d1 is complex real ext-real Element of REAL

r3 + c is ext-real Element of ExtREAL
d1 is 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

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

{ K430(b1,b2) where b1, b2 is complex Element of COMPLEX : ( b1 in {a} & b2 in a ) } is set

{ (b1 + b2) where b1, b2 is ext-real Element of ExtREAL : ( b1 in {a} & b2 in a ) } is set

{ K430(b1,b2) where b1, b2 is complex Element of COMPLEX : ( b1 in {x} & b2 in A ) } is set

{ (b1 + b2) where b1, b2 is ext-real Element of ExtREAL : ( b1 in {x} & b2 in A ) } is set

{ K430(b1,b2) where b1, b2 is complex Element of COMPLEX : ( b1 in {a} & b2 in a ) } is set

{ (b1 + b2) where b1, b2 is ext-real Element of ExtREAL : ( b1 in {a} & b2 in a ) } is set

{ 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

r3 + m is ext-real Element of ExtREAL
r3 + n is ext-real Element of ExtREAL

{ K430(b1,b2) where b1, b2 is complex Element of COMPLEX : ( b1 in {c5} & b2 in a ) } is set

{ (b1 + b2) where b1, b2 is ext-real Element of ExtREAL : ( b1 in {c5} & b2 in a ) } is set

m1 is ext-real Element of ExtREAL
oi is ext-real Element of ExtREAL

s is set

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

{ K430(b1,b2) where b1, b2 is complex Element of COMPLEX : ( b1 in {a} & b2 in a ) } is set

{ (b1 + b2) where b1, b2 is ext-real Element of ExtREAL : ( b1 in {a} & b2 in a ) } is set

{ K430(b1,b2) where b1, b2 is complex Element of COMPLEX : ( b1 in {x} & b2 in A ) } is set

{ (b1 + b2) where b1, b2 is ext-real Element of ExtREAL : ( b1 in {x} & b2 in A ) } is set

{ K430(b1,b2) where b1, b2 is complex Element of COMPLEX : ( b1 in {a} & b2 in a ) } is set

{ (b1 + b2) where b1, b2 is ext-real Element of ExtREAL : ( b1 in {a} & b2 in a ) } is set

x1 is ext-real Element of ExtREAL

{ 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

r3 + m is ext-real Element of ExtREAL

{ K430(b1,b2) where b1, b2 is complex Element of COMPLEX : ( b1 in {c5} & b2 in a ) } is set

{ (b1 + b2) where b1, b2 is ext-real Element of ExtREAL : ( b1 in {c5} & b2 in a ) } is set

].(r3 + x1),(r3 + m).] is ext-real-membered non left_end interval set
s is set

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

{ K430(b1,b2) where b1, b2 is complex Element of COMPLEX : ( b1 in {a} & b2 in a ) } is set

{ (b1 + b2) where b1, b2 is ext-real Element of ExtREAL : ( b1 in {a} & b2 in a ) } is set

{ K430(b1,b2) where b1, b2 is complex Element of COMPLEX : ( b1 in {x} & b2 in A ) } is set

{ (b1 + b2) where b1, b2 is ext-real Element of ExtREAL : ( b1 in {x} & b2 in A ) } is set

{ K430(b1,b2) where b1, b2 is complex Element of COMPLEX : ( b1 in {x} & b2 in A ) } is set

{ (b1 + b2) where b1, b2 is ext-real Element of ExtREAL : ( b1 in {x} & b2 in A ) } is set

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

a is ext-real set

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

{ K430(b1,b2) where b1, b2 is complex Element of COMPLEX : ( b1 in {x} & b2 in A ) } is set

{ (b1 + b2) where b1, b2 is ext-real Element of ExtREAL : ( b1 in {x} & b2 in A ) } is set

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

a is ext-real set

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

{ K430(b1,b2) where b1, b2 is complex Element of COMPLEX : ( b1 in {x} & b2 in A ) } is set

{ (b1 + b2) where b1, b2 is ext-real Element of ExtREAL : ( b1 in {x} & b2 in A ) } is set

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

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

(abs A) + (abs x) is complex real ext-real Element of REAL

(abs A) + (abs a) is complex real ext-real Element of REAL

(- A) + (abs a) is complex real ext-real Element of REAL

a + (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

(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

(A . x1) - 0 is complex real ext-real Element of REAL

(A . x1) + () is complex real ext-real set
abs ((A . x1) - 0) is complex real ext-real Element of REAL

x + (- 1) is complex real ext-real set

a is ext-real set

c5 is set

a is ext-real set

c5 is set

{ b1 where b1 is complex real ext-real Element of REAL : ( 0 <= b1 & b1 <= 0 ) } is set

bool () is non empty set

{ K428(b1) where b1 is complex Element of COMPLEX : b1 in A } is set

{ (- b1) where b1 is ext-real Element of ExtREAL : b1 in A } is set

{ K428(b1) where b1 is complex Element of COMPLEX : b1 in x } is set

{ (- b1) where b1 is ext-real Element of ExtREAL : b1 in x } is set

{ K428(b1) where b1 is complex Element of COMPLEX : b1 in a } is set

{ (- b1) where b1 is ext-real Element of ExtREAL : b1 in a } is set

{ K428(b1) where b1 is complex Element of COMPLEX : b1 in A } is set

{ (- b1) where b1 is ext-real Element of ExtREAL : b1 in A } is set

a is ext-real set

- a is complex set

{ K428(b1) where b1 is complex Element of COMPLEX : b1 in A } is set

{ (- b1) where b1 is ext-real Element of ExtREAL : b1 in A } is set

a is ext-real set

- a is complex set

{ K428(b1) where b1 is complex Element of COMPLEX : b1 in A } is set

{ (- b1) where b1 is ext-real Element of ExtREAL : b1 in A } is 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

{ K428(b1) where b1 is complex Element of COMPLEX : b1 in A } is set

{ (- b1) where b1 is ext-real Element of ExtREAL : b1 in A } is 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

{ 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

{ 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

- (- (upper_bound (A))) is complex real ext-real Element of 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

{ 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
- (- (lower_bound (A))) is complex real ext-real Element of REAL

{ K428(b1) where b1 is complex Element of COMPLEX : b1 in A } is set

{ (- b1) where b1 is ext-real Element of ExtREAL : b1 in A } is set

a is set

a is set
(- x) . a 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

{ 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

{ K428(b1) where b1 is complex Element of COMPLEX : b1 in A } is set

{ (- b1) where b1 is ext-real Element of ExtREAL : b1 in A } is 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

{ K430(b1,b2) where b1, b2 is complex Element of COMPLEX : ( b1 in {x} & b2 in A ) } is set

{ (b1