One thing that bugs me about this, is that a lot of theorems seem to be formulated backwards. To give an example: Theorem 9.1. Let f be a continuous real-value

One thing that bugs me about this, is that a lot of theorems seem to be formulated backwards. To give an example: Theorem 9.1. Let f be a continuous real-valued function. Let y be a real number. Let b ≤ c be real numbers with f(b) ≤ y ≤ f(c). Then f(x) = y for some x in [b, c]. Why is this well-formed? Once you say "Let y be a real number", I'm free to pick any real number, which means that there might not be a b and c such that f(b) ≤ y ≤ f(c). Now, I obviously understand what is said, but shouldn't this be formulated more like: Let f be a continuous real-valued function. Let b ≤ c be real numbers from the domain of f. Let y be a real number in the closed interval bounded by f(b) and f(c) ([f(b), f(c)] or [f(c), f(b)], depending on whether f(b) ≤ f(c) or not). Then there exists an x in [b, c] such, that f(x) = y. The way this and other theorems, definitions, etc. are formulated in the article bugs me, because I must go back and re-qualify variables based on information deduced from things introduced, after the variable in question was introduced.