Some Properties of the Intervals MML Identifier: MEASURE6.

and notation for this paper. The scheme FunctXD YD concerns a non empty set A, a non empty set B, and a binary predicate P, and states that: There exists a function F from A into B such that for every element x of A holds P[x,F(x)] provided the following condition is satisfied: • For every element x of A there exists an element y of B such that P[x,y]. Let X, Y be non empty sets. Note that Y X is non empty. We now state a number of propositions: (1) There exists a function F from ¦ into [: ¦ , ¦:] such that F is one-to-one and domF = ¦ and rng F = [: ¦ , ¦:]. (2) For every function F from ¦ into ¤ such that F is non-negative holds 0 § ≤ � F. (3) Let F be a function from ¦ into ¤ and let x be a Real number. Suppose there exists a natural number n such that x ≤ F(n) and F is non-negative. Then x ≤ � F. (4) For every Real number x such that there exists a Real number y such that y < x holds x � = −∞. (5) For every Real number x such that there exists a Real number y such that x < y holds x � = +∞. (6) For all Real numbers x, y holds x ≤ y iff x < y or x = y. (7) Let x, y be Real numbers and let p, q be real numbers. If x = p and y = q, then p ≤ q iff x ≤ y. (8) For all Real numbers x, y such that x is a real number holds (y−x)+x = y and (y + x) − x = y. (9) For all Real numbers x, y such that x ∈ ¤ holds x + y = y + x