 All we have discussed so far is the relative types of \(\phi\) and \(\chi\). The Axiom of Reducibility guarantees that there is a predicative \(\chi\) co-extensive with any \(\psi\) in the defining condition of a class. To justify use of the class term \(\{x \mid \psi (x) \}\) one must then just show that there is some function that has the higher-order property \(\phi\). This is the step comparable to the proof that a definite description is proper, i.e., true of exactly one thing, that justifies using that description as a singular term.