 The theory NF which we obtain can be described briefly (but deceptively) as being the first-order untyped theory with equality and membership having the same axioms as TST but without the distinctions of type. If this is not read very carefully, it may be seen as implying that we have adopted the comprehension axioms of naive set theory,