$$\ast54.3.  \vdash 2 = \hat\alpha\{ (\exists x) \> .\>
x\in\alpha \> . \> \alpha - \iota`x\in 1 \}$$