:: MEASURE6 semantic presentation

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

c

(Ser A) . c

c

A . (c

((Ser A) . c

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

c

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

c

c

SUM c

Ser c

rng (Ser c

sup (rng (Ser c

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

c

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

c

(c

2 " is complex real ext-real non negative set

2 " is non empty complex real ext-real positive non negative set

(c

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

c

r3 is ext-real set

dom (Ser c

x1 is set

(Ser c

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 c

c

((Ser c

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 c

c

((Ser c

(c

2 " is complex real ext-real non negative set

2 " is non empty complex real ext-real positive non negative set

(c

(c

((Ser c

((Ser c

(((Ser c

(Ser c

((Ser c

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 c

c

((Ser c

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

{ b

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

{ b

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

{ b

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

{ b

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

{ b

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

{ b

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

{ b

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

x ++ A is ext-real-membered set

{ (b

a is complex real ext-real Element of REAL

a is complex Element of COMPLEX

c

a + c

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

c

a + c

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

{x} ++ A is ext-real-membered set

{ (b

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

{x} ++ A is ext-real-membered set

{ (b

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

c

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

{x} ++ A is ext-real-membered set

{ (b

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

{(- x)} ++ (A,x) is ext-real-membered set

{ (b

(- x) ++ (A,x) is ext-real-membered set

a is set

a is complex real ext-real Element of REAL

c

(- x) + c

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

c

c

c

r3 is complex real ext-real Element of REAL

(- x) + c

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

{A} ++ x is ext-real-membered set

{ (b

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

c

A + c

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

{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

{ (b

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

{x} ++ A is ext-real-membered set

{ (b

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

c

(a,c

{c

{c

{ K430(b

{c

{ (b

c

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

{ b

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

{r3} ++ a is ext-real-membered set

{ (b

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

{ b

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

{a} ++ a is ext-real-membered set

{ (b

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

{x} ++ A is ext-real-membered set

{ (b

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

{a} ++ a is ext-real-membered set

{ (b

a ++ a is ext-real-membered set

c

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

{ b

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,c

{c

{c

{ K430(b

{c

{ (b

c

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

c

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

- c

c + (- c

c

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

{a} ++ a is ext-real-membered set

{ (b

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

{x} ++ A is ext-real-membered set

{ (b

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

{a} ++ a is ext-real-membered set

{ (b

a ++ a is ext-real-membered set

c

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

{ b

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,c

{c

{c

{ K430(b

{c

{ (b

c

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

c

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

- c

c + (- c

c

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

{a} ++ a is ext-real-membered set

{ (b

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

{x} ++ A is ext-real-membered set

{ (b

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

{a} ++ a is ext-real-membered set

{ (b

a ++ a is ext-real-membered set

c

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

{ b

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,c

{c

{c

{ K430(b

{c

{ (b

c

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

c

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

- c

c + (- c

c

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

{a} ++ a is ext-real-membered set

{ (b

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

{x} ++ A is ext-real-membered set

{ (b

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

{x} ++ A is ext-real-membered set

{ (b

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)

c

c

- a is ext-real set

c

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

c

x + c

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

{x} ++ A is ext-real-membered set

{ (b

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)

c

c

- a is ext-real set

c

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

c

x + c

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

{x} ++ A is ext-real-membered set

{ (b

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

c

c

c

(c

- (c

(c

sup (A,x) is ext-real Element of ExtREAL

(sup (A,x)) - (c

(sup (A,x)) + (- (c

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

c

r3 is set

c

c

r3 is set

x1 is set

r3 is set

x1 is set

a is set

a is set

a is set

c

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

c

(A,x,c

[:(bool x),(bool A):] is Relation-like non empty set

bool [:(bool x),(bool A):] is non empty set

(A,x,c

bool (bool A) is non empty set

meet ((A,x,c

c

r3 is set

(A,x,c

c

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

c

A . c

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

c

A . c

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

{ b

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

-- A is ext-real-membered set

{ (- b

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

-- x is ext-real-membered set

{ (- b

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

-- a is ext-real-membered set

{ (- b

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

-- A is ext-real-membered set

{ (- b

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

c

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

-- A is ext-real-membered set

{ (- b

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

c

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

-- A is ext-real-membered set

{ (- b

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

{ K428(b

-- (A) is ext-real-membered set

{ (- b

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

-- A is ext-real-membered set

{ (- b

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

{ K428(b

-- (A) is ext-real-membered set

{ (- b

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

-- A is non empty ext-real-membered set

{ (- b

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

-- (A) is non empty ext-real-membered set

{ (- b

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

-- A is non empty ext-real-membered set

{ (- b

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

-- (A) is non empty ext-real-membered set

{ (- b

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

-- A is ext-real-membered set

{ (- b

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

c

x . c

- (x . c

- (x . c

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

{ K428(b

-- (A) is ext-real-membered set

{ (- b

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

-- A is ext-real-membered set

{ (- b

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

{ K428(b

-- (A) is ext-real-membered set

{ (- b

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

{x} ++ A is ext-real-membered set

{ (b