 for each formula \(\phi\). But we have not. We have only adopted those axioms for formulas \(\phi\) which can be obtained from formulas of TST by dropping distinctions of type between the variables (without introducing any identifications between variables of different types). For example, there is no way that \(x \not\in x\) can be obtained by dropping distinctions of type from a formula of TST, without identifying two variables of different type. Formulas of the untyped language of set theory in which it is possible to assign a type to each variable (the same type wherever it occurs) in such a way as to get a formula of TST are said to be stratified. The axioms of NF are strong extensionality (no non-sets) and stratified comprehension.