of j. Now exists (because j appears applied only to free variables and constants), belongs to , and contains exactly those y which satisfy the original formula in the model of NFU. has this extension in the model of NFU (the application of j corrects for the different definition of membership in the model of NFU). This establishes that Stratified Comprehension holds in the model of NFU. To see that weak Extensionality holds is straightforward: each nonempty element of inherits a unique extension from the nonstandard model, the empty set inherits its usual extension as well, and all other objects are urelements. The basic idea is that the automorphism j codes the "power set" of our "universe" into its externally isomorphic copy inside our "universe." The remaining objects not coding subsets of the universe are treated as urelements. If is a natural number n, one gets a model of NFU which claims that the universe is finite (it is externally infinite, of course). If is infinite and the Choice holds in the nonstandard model of ZFC, one obtains a model of NFU + Infinity + Choice. Self-sufficiency of mathematical foundations in NFU For philosophical reasons, it is important to note that it is not necessary to work in ZFC or any related system to carry out this proof. A common argument against the use of NFU as a foundation for mathematics is that the reasons for relying on it have to do with the intuition that ZFC is correct. It is sufficient to accept TST (in fact TSTU). In outline: take the type theory TSTU (allowing urelements in each positive type) as a metatheory and consider the theory of set models of TSTU in TSTU (these models will be sequences of sets (all of the same type in the metatheory) with embeddings of each into coding embeddings of the power set of into in a type-respecting manner). Given an embedding of into (identifying elements of the base "type" with subsets of the base type), embeddings may be defined from each "type" into its successor in a natural way. This can be generalized to transfinite sequences with care. Note that the construction of such sequences of sets is limited by the size of the type in which they are being constructed; this prevents TSTU from proving its own consistency (TSTU + Infinity can prove the consistency of TSTU; to prove the