. The triviality of the T operation is only a seeming one; it is easy to show that T is a strictly monotone (order-preserving) operation on the ordinals. Now the lemma on order types may be restated in a stratified manner: the order type of the natural order on the ordinals is or depending on which pair is used (we assume the type level pair hereinafter). From this one may deduce that the order type on the ordinals is , and thus . Hence the T operation is not a function; there cannot be a strictly monotone set map from ordinals to ordinals which sends an ordinal downward! Since T is monotone, we have , a "descending sequence" in the ordinals which cannot be a set. One might assert that this result shows that no model of NF(U) is "standard", since the ordinals in any model of NFU are externally not well-ordered. One need not take a position on this, but can note that it is also a theorem of NFU that any set model of NFU has non-well-ordered "ordinals"; NFU does not conclude that the universe V is a model of NFU, despite V being a set, because the membership relation is not a set relation. For a further development of mathematics in NFU, with a comparison to the development of the same in ZFC, see implementation of mathematics in set theory. The system ML (Mathematical Logic) ML is an extension of NF that includes proper classes as well as sets. The set theory of the 1940 first edition of Quine's Mathematical Logic married NF to the proper classes of NBG set theory and included an axiom schema of unrestricted comprehension for proper classes. However proved that the system presented in Mathematical Logic was subject to the Burali-Forti paradox. This result does not apply to NF. showed how to amend Quine's axioms for ML so as to avoid this problem, and Quine included the resulting axiomatization in the 1951 second and final edition of Mathematical Logic. Wang proved that if NF is consistent then so is the revised ML, and also showed that the consistency of the revised ML implies the consistency of NF. That is, NF and the revised ML are equiconsistent. Models of NFU Where the starting point for the metamathematics of Zermelo-Fraenkel set theory is the easy-to-formalize intuition of the cumulative hierarchy, the non-well-foundedness of NF