The Graph Reading of a Formula Tree Is Predicative and Agrees with Its Reading, So the Reading Is Predicative

Let $\varphi$ be a formula tree with $n$ set variables (Formula Trees with Values: Syntax, Two Readings, and Definedness (i)).

(i) Graph reading. If $\varphi$ is well scoped and its side conditions hold, then its graph reading is the reading of a predicative formula whose free variables are among $x_0, \dots, x_{n-1}$ and class variables standing for the parameters of $\varphi$.

(ii) Agreement. Under every assignment of sets to $x_0, \dots, x_{n-1}$ at which $\varphi$ uses its values properly, the graph reading of $\varphi$ holds if and only if its reading holds.

(iii) Reading. If $\varphi$ is well scoped, its side conditions hold, and $\varphi$ uses its values properly under every assignment of sets to $x_0, \dots, x_{n-1}$, then its reading is the reading of a predicative formula whose free variables are among $x_0, \dots, x_{n-1}$ and class variables standing for the parameters of $\varphi$.