:: MEASURE5 semantic presentation

K32(REAL) is non empty set

K33(NAT,ExtREAL) is set
K32(K33(NAT,ExtREAL)) is non empty set
K32(ExtREAL) is non empty 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

{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= -infty & not +infty <= b1 ) } is set

b is V24() real ext-real set

b is V24() real ext-real set

{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= X & not a <= b1 ) } is set

b is set

a is V24() real ext-real set

a is V24() real ext-real set

-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

{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= -infty & not +infty <= b1 ) } is set

{ b1 where b1 is ext-real Element of ExtREAL : ( 0 <= b1 & b1 <= 1 ) } is set
+infty is non empty non real ext-real positive non negative Element of ExtREAL

{ b1 where b1 is ext-real Element of ExtREAL : ( 0 <= b1 & not +infty <= b1 ) } is set
-infty is non empty non real ext-real non positive negative Element of ExtREAL

{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= -infty & b1 <= 1 ) } is set

{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= a & not b <= b1 ) } is set

a is V24() real ext-real set
b is V24() real ext-real set

{ b1 where b1 is ext-real Element of ExtREAL : ( a <= b1 & b1 <= b ) } is set

a is V24() real ext-real set

{ b1 where b1 is ext-real Element of ExtREAL : ( a <= b1 & not b <= b1 ) } is set

b is V24() real ext-real set

{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= a & b1 <= b ) } is set

{ b1 where b1 is ext-real Element of ExtREAL : ( a <= b1 & b1 <= b ) } is set

].(inf X),(sup X).] is ext-real-membered non left_end interval set
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= inf X & b1 <= sup X ) } is set

[.(inf X),(sup X).[ is ext-real-membered non right_end interval set
{ b1 where b1 is ext-real Element of ExtREAL : ( inf X <= b1 & not sup X <= b1 ) } is set
a is ext-real set
b is ext-real set

{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= a & not b <= b1 ) } is set

-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

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
c6 is V24() real ext-real Element of REAL
c7 is ext-real Element of ExtREAL
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
c6 is ext-real Element of ExtREAL
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
c6 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

c6 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

sup {X,a} is ext-real set

(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

{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= X & not a <= b1 ) } is set
((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

{ b1 where b1 is ext-real Element of ExtREAL : ( X <= b1 & b1 <= a ) } is set
([.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

{ b1 where b1 is ext-real Element of ExtREAL : ( X <= b1 & not a <= b1 ) } is set
([.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

{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= X & b1 <= a ) } is set
(].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

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

{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= a & not b <= b1 ) } is set

{ b1 where b1 is ext-real Element of ExtREAL : ( a <= b1 & b1 <= b ) } is set

{ b1 where b1 is ext-real Element of ExtREAL : ( a <= b1 & not b <= b1 ) } is set

{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= a & b1 <= b ) } is set

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

{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= 0. & not 0. <= b1 ) } is set
({}) is ext-real Element of ExtREAL

(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

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

{ b1 where b1 is ext-real Element of ExtREAL : ( X <= b1 & b1 <= a ) } is set

(b) is ext-real Element of ExtREAL

(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 ext-real Element of ExtREAL
(a) is ext-real Element of ExtREAL

(X) is ext-real Element of ExtREAL

a is V24() real ext-real set
b is V24() real ext-real set

{ b1 where b1 is ext-real Element of ExtREAL : ( a <= b1 & b1 <= b ) } is set
a is V24() real ext-real Element of REAL
b is V24() real ext-real Element of REAL

{ b1 where b1 is ext-real Element of ExtREAL : ( a <= b1 & b1 <= b ) } is set
a is V24() real ext-real Element of REAL
b is V24() real ext-real Element of REAL

{ b1 where b1 is ext-real Element of ExtREAL : ( a <= b1 & b1 <= b ) } is set