order type of the restriction of to is ; then define as the element with index in the natural order on the elements of . The cardinal is the element with index in the natural order on all infinite cardinals (which is a well-ordering, see above). Note that follows immediately from this definition. In all these constructions, notice that the type of the index is two higher (with type-level ordered pair) than the type of . Each set A of ZFC has a transitive closure (the intersection of all transitive sets which contains A). By the axiom of foundation, the restriction of the membership relation to the transitive closure of A is a well-founded relation. The relation is either empty or has A as its top element, so this relation is a set picture. It can be proved in ZFC that every set picture is isomorphic to some . This suggests that (an initial segment of) the cumulative hierarchy can be studied by considering the isomorphism classes of set pictures. These isomorphism classes are sets and make up a set in NFU. There is a natural set relation analogous to membership on isomorphism classes of set pictures: if is a set picture, write for its isomorphism class and define as holding if is the isomorphism class of the restriction of y to the downward closure of one of the elements of the preimage under y of the top element of y. The relation E is a set relation, and it is straightforward to prove that it is well-founded and extensional. If the definition of E is confusing, it can be deduced from the observation that it is induced by precisely the relationship which holds between the set picture associated with A and the set picture associated with B when in the usual set theory. There is a T operation on isomorphism classes of set pictures analogous to the T operation on ordinals: if x is a set picture, so is . Define as . It is easy to see that . An axiom of extensionality for this simulated set theory follows from E's extensionality. From its well-foundedness follows an axiom of foundation. There remains the question of what comprehension axiom E may have. Consider any collection of set pictures (collection of set pictures whose fields are made up entirely of singletons). Since each is one type higher than x (using