 This means that we should be able to specify when a type \(n + 2\) set \(A^{n+2}\) refines a type \(n + 1\) set \(A^{n+1}\): each (type \(n + 1)\) element of \(A^{n+2}\) should refine a (type \(n)\) element of \(A^{n+1}\), and each element of \(A^{n+1}\) should be refined by one or more elements of \(A^{n+2}\). Along with the information that the type 0 object \(u\) refines both of the elements of type 1, this gives a complete recursive definition of the notion of refinement of a type \(n\) set by a type \(n + 1\) set. Each type \(n + 1\) set refines a unique type \(n\) set but may be refined by many type \(n + 2\) sets. (The “hereditarily finite” sets without \(u\) in their transitive closure are refined by just one precisely analogous set at the next higher level.) Define a general relation \(x \sim y\) on all elements of the model of set theory as holding when \(x = y\) (if they are of the same type) or if there is a chain of refinements leading from the one of \(x, y\) of lower type to the one of higher type.