  The best way to illustrate this is by considering ordinals \((=\) isomorphism classes of wellorderings) in NF. For any ordinal \(\alpha\) the order type of the set (and it is a set) of the ordinals below \(\alpha\) is wellordered. In ZF one can prove that the wellordering of the ordinals below \(\alpha\) is of length \(\alpha\). In NF one cannot prove this equation for arbitrary \(\alpha\) since the formula in the set abstract whose extension is the graph of the isomorphism is not stratified for any implementation of ordered pair. Now any wellordering \(R\) of a set \(A\) to length \(\alpha\) gives rise to a wellordering of \(\{\{\{a\}\} : a \in A\}\), and if instead one tries to prove (in NF) that the ordinals below \(\alpha\) are isomorphic to the wellordering of length \(\alpha\) decorated with curly brackets, one finds that the very assertion that there is an isomorphism between these two wellorderings comes out stratified or unstratified depending on one’s choice of implementation of ordered pair! This is because, in some sense, the applications of the pairing function are two deep in wellordering of the ordinals below \(\alpha\), but only one deep in the wellordering of the set of double singletons. If we use Quine ordered pairs, the assertion is stratified – and provable. If one uses Wiener-Kuratowski ordered pairs then the assertion is unstratified and refutable. However if one uses Wiener-Kuratowki ordered pairs there is instead the assertion that the ordinals below \(\alpha\) are isomorphic to the obvious wellordering of \(\{\{\{\{\{a\}\}\}\} : a \in A\}\), which comes out stratified (and provable). In general for each implementation of ordered pair there is a depth of nesting of curly brackets which will make a version of this equality come out stratified and true. This does not work with deviant implementations of ordered pair under which “\(\langle x, y\rangle = z\)” is unstratified or even with those which are stratified but give the variables \(x\) and \(y\) different types. Use of such implementations of ordered pairs results in certain sets not being the same size as themselves!