:: MEASURE5 semantic presentation

REAL is non empty V5() V36() complex-membered ext-real-membered real-membered V47() non bounded_below non bounded_above interval set

NAT is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V47() bounded_below Element of K32(REAL)

K32(REAL) is non empty set

ExtREAL is non empty ext-real-membered interval set

K33(NAT,ExtREAL) is set

K32(K33(NAT,ExtREAL)) is non empty set

K32(ExtREAL) is non empty set

omega is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V47() bounded_below set

K32(omega) is non empty 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

{+infty,-infty} is non empty V36() ext-real-membered left_end right_end set

REAL \/ {+infty,-infty} is non empty ext-real-membered set

{} is empty V36() V40() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V47() bounded_below bounded_above real-bounded interval set

the empty V36() V40() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V47() bounded_below bounded_above real-bounded interval set is empty V36() V40() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V47() bounded_below bounded_above real-bounded interval set

].-infty,+infty.[ is complex-membered ext-real-membered real-membered non left_end non right_end interval set

{ b

0 is empty natural V24() real ext-real non positive non negative V36() V40() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V47() bounded_below bounded_above real-bounded interval Element of NAT

X is complex-membered ext-real-membered real-membered Element of K32(REAL)

a is complex-membered ext-real-membered real-membered Element of K32(REAL)

b is V24() real ext-real set

a is ext-real Element of ExtREAL

b is V24() real ext-real set

a is ext-real Element of ExtREAL

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 set

{ b

].X,a.[ is complex-membered ext-real-membered real-membered non left_end non right_end interval Element of K32(REAL)

b is set

b is complex-membered ext-real-membered real-membered Element of K32(REAL)

].X,a.[ is complex-membered ext-real-membered real-membered non left_end non right_end interval Element of K32(REAL)

a is ext-real Element of ExtREAL

b is ext-real Element of ExtREAL

a is V24() real ext-real set

b is ext-real Element of ExtREAL

a is V24() real ext-real set

b is ext-real 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,+infty) is complex-membered ext-real-membered real-membered non left_end non right_end interval Element of K32(REAL)

{ b

1 is non empty natural V24() real ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end bounded_below Element of NAT

[.0,1.] is complex-membered ext-real-membered real-membered interval Element of K32(REAL)

{ b

+infty is non empty non real ext-real positive non negative Element of ExtREAL

[.0,+infty.[ is complex-membered ext-real-membered real-membered non right_end interval Element of K32(REAL)

{ b

-infty is non empty non real ext-real non positive negative Element of ExtREAL

1 is non empty natural V24() real ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end bounded_below Element of NAT

].-infty,1.] is complex-membered ext-real-membered real-membered non left_end interval Element of K32(REAL)

{ b

X is complex-membered ext-real-membered real-membered Element of K32(REAL)

a is ext-real Element of ExtREAL

b is ext-real Element of ExtREAL

(a,b) is complex-membered ext-real-membered real-membered non left_end non right_end interval Element of K32(REAL)

{ b

X is complex-membered ext-real-membered real-membered Element of K32(REAL)

a is V24() real ext-real set

b is V24() real ext-real set

[.a,b.] is complex-membered ext-real-membered real-membered interval Element of K32(REAL)

{ b

X is complex-membered ext-real-membered real-membered Element of K32(REAL)

a is V24() real ext-real set

b is ext-real Element of ExtREAL

[.a,b.[ is complex-membered ext-real-membered real-membered non right_end interval Element of K32(REAL)

{ b

X is complex-membered ext-real-membered real-membered Element of K32(REAL)

a is ext-real Element of ExtREAL

b is V24() real ext-real set

].a,b.] is complex-membered ext-real-membered real-membered non left_end interval Element of K32(REAL)

{ b

X is complex-membered ext-real-membered real-membered interval Element of K32(REAL)

inf X is ext-real Element of ExtREAL

sup X is ext-real Element of ExtREAL

a is ext-real Element of ExtREAL

b is ext-real Element of ExtREAL

[.a,b.] is ext-real-membered interval set

{ b

inf X is ext-real Element of ExtREAL

sup X is ext-real Element of ExtREAL

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

{ b

inf X is ext-real Element of ExtREAL

sup X is ext-real Element of ExtREAL

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

{ b

a is ext-real set

b is ext-real set

].a,b.[ is complex-membered ext-real-membered real-membered non left_end non right_end interval Element of K32(REAL)

{ b

a is ext-real Element of ExtREAL

b is ext-real Element of ExtREAL

a is ext-real Element of ExtREAL

X is ext-real 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,+infty} is non empty V36() ext-real-membered left_end right_end set

b is V24() real ext-real Element of REAL

a is V24() real ext-real Element of REAL

b is V24() real ext-real set

c

c

b is V24() real ext-real Element of REAL

a is V24() real ext-real set

b is V24() real ext-real Element of REAL

c

b is V24() real ext-real Element of REAL

a is V24() real ext-real set

b is V24() real ext-real Element of REAL

c

0. is empty ext-real non positive non negative V36() V40() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V47() bounded_below bounded_above real-bounded interval Element of ExtREAL

a is ext-real Element of ExtREAL

X is ext-real Element of ExtREAL

b is ext-real Element of ExtREAL

min (a,b) is ext-real set

{a,b} is non empty V36() ext-real-membered left_end right_end set

inf {a,b} is ext-real set

a is ext-real Element of ExtREAL

a is ext-real Element of ExtREAL

b is ext-real Element of ExtREAL

c

b is ext-real Element of ExtREAL

X is ext-real Element of ExtREAL

a is ext-real Element of ExtREAL

max (X,a) is ext-real set

{X,a} is non empty V36() ext-real-membered left_end right_end set

a is ext-real Element of ExtREAL

b is ext-real Element of ExtREAL

sup {X,a} is ext-real set

X is ext-real-membered set

sup X is ext-real Element of ExtREAL

inf X is ext-real Element of ExtREAL

(sup X) - (inf X) is ext-real Element of ExtREAL

K166((inf X)) is ext-real set

K165((sup X),K166((inf X))) is ext-real set

0. is empty ext-real non positive non negative V36() V40() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V47() bounded_below bounded_above real-bounded interval Element of ExtREAL

a is ext-real Element of ExtREAL

X 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 K32(REAL)

{ b

((X,a)) is ext-real Element of ExtREAL

a - X is ext-real Element of ExtREAL

K166(X) is ext-real set

K165(a,K166(X)) is ext-real set

sup (X,a) is ext-real Element of ExtREAL

inf (X,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 interval set

{ b

([.X,a.]) is ext-real Element of ExtREAL

a - X is ext-real Element of ExtREAL

K166(X) is ext-real set

K165(a,K166(X)) is ext-real set

sup [.X,a.] is ext-real Element of ExtREAL

inf [.X,a.] is ext-real Element of ExtREAL

a is ext-real Element of ExtREAL

X is ext-real Element of ExtREAL

[.X,a.[ is ext-real-membered non right_end interval set

{ b

([.X,a.[) is ext-real Element of ExtREAL

a - X is ext-real Element of ExtREAL

K166(X) is ext-real set

K165(a,K166(X)) is ext-real set

sup [.X,a.[ is ext-real Element of ExtREAL

inf [.X,a.[ is ext-real Element of ExtREAL

a is ext-real Element of ExtREAL

X is ext-real Element of ExtREAL

].X,a.] is ext-real-membered non left_end interval set

{ b

(].X,a.]) is ext-real Element of ExtREAL

a - X is ext-real Element of ExtREAL

K166(X) is ext-real set

K165(a,K166(X)) is ext-real set

sup ].X,a.] is ext-real Element of ExtREAL

inf ].X,a.] is ext-real 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

X is complex-membered ext-real-membered real-membered interval Element of K32(REAL)

(X) is ext-real Element of ExtREAL

a is ext-real Element of ExtREAL

b is ext-real Element of ExtREAL

(a,b) is complex-membered ext-real-membered real-membered non left_end non right_end interval Element of K32(REAL)

{ b

[.a,b.] is ext-real-membered interval set

{ b

[.a,b.[ is ext-real-membered non right_end interval set

{ b

].a,b.] is ext-real-membered non left_end interval set

{ b

sup X is ext-real Element of ExtREAL

inf X is ext-real Element of ExtREAL

b - a is ext-real Element of ExtREAL

K166(a) is ext-real set

K165(b,K166(a)) is ext-real set

X is complex-membered ext-real-membered real-membered Element of K32(REAL)

(0.,0.) is empty proper V36() V40() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V47() non left_end non right_end bounded_below bounded_above real-bounded interval Element of K32(REAL)

{ b

({}) is ext-real Element of ExtREAL

X is complex-membered ext-real-membered real-membered interval Element of K32(REAL)

(X) is ext-real Element of ExtREAL

inf X is ext-real Element of ExtREAL

sup X is ext-real Element of ExtREAL

(sup X) - (inf X) is ext-real Element of ExtREAL

K166((inf X)) is ext-real set

K165((sup X),K166((inf X))) is ext-real set

X is complex-membered ext-real-membered real-membered interval Element of K32(REAL)

(X) is ext-real Element of ExtREAL

a is complex-membered ext-real-membered real-membered interval Element of K32(REAL)

(a) is ext-real Element of ExtREAL

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

K166((inf a)) is ext-real set

K165((sup a),K166((inf a))) is ext-real set

sup X is ext-real Element of ExtREAL

inf X is ext-real Element of ExtREAL

(sup X) - (inf X) is ext-real Element of ExtREAL

K166((inf X)) is ext-real set

K165((sup X),K166((inf X))) is ext-real set

X is ext-real Element of ExtREAL

a is ext-real Element of ExtREAL

[.X,a.] is ext-real-membered interval set

{ b

b is complex-membered ext-real-membered real-membered interval Element of K32(REAL)

(b) is ext-real Element of ExtREAL

a is complex-membered ext-real-membered real-membered interval Element of K32(REAL)

(a) is ext-real Element of ExtREAL

{X} is non empty V36() ext-real-membered left_end right_end set

inf a is ext-real Element of ExtREAL

sup a is ext-real Element of ExtREAL

X - X is ext-real Element of ExtREAL

K166(X) is ext-real set

K165(X,K166(X)) is ext-real set

X is complex-membered ext-real-membered real-membered interval Element of K32(REAL)

a is complex-membered ext-real-membered real-membered interval Element of K32(REAL)

(X) is ext-real Element of ExtREAL

(a) is ext-real Element of ExtREAL

X is complex-membered ext-real-membered real-membered interval Element of K32(REAL)

(X) is ext-real Element of ExtREAL

X is complex-membered ext-real-membered real-membered Element of K32(REAL)

a is V24() real ext-real set

b is V24() real ext-real set

[.a,b.] is complex-membered ext-real-membered real-membered interval Element of K32(REAL)

{ b

a is V24() real ext-real Element of REAL

b is V24() real ext-real Element of REAL

[.a,b.] is complex-membered ext-real-membered real-membered interval Element of K32(REAL)

{ b

a is V24() real ext-real Element of REAL

b is V24() real ext-real Element of REAL

[.a,b.] is complex-membered ext-real-membered real-membered interval Element of K32(REAL)

{ b