 Suppose a mathematician wants to convince someone about the truth of Bolzano’s Theorem “If a continuous function on the reals has negative values as well as positive values inside an interval, then it has a root in that interval”. They would start with the ordered field of real numbers. It would be (thought to be) clear what this means because the second-order axiomatization of the field is categorical. Then they would take an arbitrary continuous function f on this field such that it has values of opposite sign inside a fixed interval \((a,b)\). It would be clear what this means because second-order logic has variables for functions. Let \(c,d\in (a,b)\) such that \(f(c)&lt;0\) and \(f(d)&gt;0\). Without loss of generality, \(c&lt;d\). Let \(X=\{e\in(a,b) : f(e)&lt;0\}\). Since we have relation variables for subsets of the domain, we can think of X simply as a value of such a relation variable. It is obvious that X exists, but a priori we could have imposed contradictory conditions on X (e.g., \(X=\{e : e\notin X\}\)) and then we should not be able to claim that it exists. However, in this case the Comprehension Axiom Schema implies that X exists. Clearly, \(X\ne\emptyset\) and X is bounded from above by d. One of the second-order axioms characterizing the field of real numbers is that every non-empty set which is bounded from above has a supremum. Thus we can let z to be the supremum of X. Now it follows from basic properties of continuous functions that \(f(z)=0\).