= Solution
\b[This encoding works.] Use three distinct tags $0,1,2$ and the <ordered pair> construction already proved <injective>. In the <set>
$$
\{\langle0,a\rangle,\langle1,b\rangle,\langle2,c\rangle\},
$$
exactly one member has first coordinate $0$, exactly one has first coordinate $1$, and exactly one has first coordinate $2$. <Equality> of two such <sets> therefore matches the members carrying each tag. <Injectivity> of the <ordered pair> construction then gives <equality> of $a$, of $b$ and of $c$, respectively.
This is a <tagged encoding of a finite tuple>. It remains valid when coordinates coincide with one another or with tags: the <equality> criterion for <ordered pairs> still distinguishes their first coordinates. <Finite set> formation using pairing and <union> makes the encoding a <set>.
Back to article page
