 Of these set theories, only NFU with Infinity, Choice and possibly further strong axioms of infinity (of which more anon) is really mathematically serviceable. We examine the construction of models of this theory and the way mathematics works inside this theory. A source for this development is Holmes 1998. Rosser 1973 develops the foundations of mathematics in NF: it can adapted to NFU fairly easily).