 Solution

This encoding works. Use three distinct tags $0,1,2$ and the ordered pair construction already proved injective. In the setexactly 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.