Past exam of the logic and set theory course of the University of Oxford / 2008 / B / 6 / 4

This encoding works, interpreting the outer three-coordinate brackets by the nested ordered pair convention established in item 1. Equality of the outer ordered triples givesFor any fixed set $k$, the map $x\mapsto \{k,x\}$ is injective. If $x=k$, equality $\{k,x\}=\{k,y\}$ makes the right-hand side a singleton and forces $y=k$. If $x\ne k$, membership of $x$ in $\{k,y\}$ forces $x=y$. Applying this argument with $k=0,1,2$ recovers the respective coordinates.

The outer brackets must encode an ordered triple, rather than an unordered set of three doubletons. The source uses three-coordinate angle brackets here; using the successful convention of item 1 makes their meaning explicit and supplies a genuine construction.