the Kuratowski ordered pair is two types higher than its projections, while the Wiener ordered pair is three types higher. It is common to postulate the existence of a type-level ordered pair (a pair which is the same type as its projections) in NFU. It is convenient to use the Kuratowski pair in both systems until the use of type-level pairs can be formally justified. The internal details of these definitions have nothing to do with their actual mathematical function. For any notion of ordered pair, the thing that matters is that it satisfies the defining condition …and that it be reasonably easy to collect ordered pairs into sets. Relations Relations are sets whose members are all ordered pairs. Where possible, a relation (understood as a binary predicate) is implemented as (which may be written as ). When is a relation, the notation means . In ZFC, some relations (such as the general equality relation or subset relation on sets) are 'too large' to be sets (but may be harmlessly reified as proper classes). In NFU, some relations (such as the membership relation) are not sets because their definitions are not stratified: in , and would need to have the same type (because they appear as projections of the same pair), but also successive types (because is considered as an element of ). Related definitions Let and be given binary relations. Then the following concepts are useful: The converse of is the relation . The domain of is the set . The range of is the domain of the converse of . That is, the set . The field of is the union of the domain and range of . The preimage of a member of the field of is the set (used in the definition of 'well-founded' below.) The downward closure of a member of the field of is the smallest set containing , and containing each for each (i.e., including the preimage of each of its elements with respect to as a subset.) The relative product of and is the relation . Notice that with our formal definition of a binary relation, the range and codomain of a relation are not distinguished. This could be done by representing a relation with codomain as , but our development will not require this. In ZFC, any relation whose domain is a subset of a set and whose range is a