 We illustrate the usefulness of the description operator with a small example. Suppose we have formalized the theory of real numbers, and our theory has constants \(1_{\varrho}\) and \(\times_{\varrho \varrho \varrho}\) to represent the number 1 and the multiplication function, respectively. (Here \(\varrho\) is the type of real numbers.) To represent the multiplicative inverse function, we can define the wff \(\textrm{INV}_{\varrho \varrho}\) as 