subset of a set will be a set, since the Cartesian product is a set (being a subclass of ), and Separation provides for the existence of . In NFU, some relations with global scope (such as equality and subset) can be implemented as sets. In NFU, bear in mind that and are three types lower than in (one type lower if a type-level ordered pair is used). Properties and kinds of relations A binary relation is: Reflexive if for every in the field of . Symmetric if . Transitive if . Antisymmetric if . Well-founded if for every set which meets the field of , whose preimage under does not meet . Extensional if for every in the field of , if and only if and have the same preimage under . Relations having certain combinations of the above properties have standard names. A binary relation is: An equivalence relation if is reflexive, symmetric, and transitive. A partial order if is reflexive, antisymmetric, and transitive. A linear order if is a partial order and for every in the field of , either or . A well-ordering if is a linear order and well-founded. A set picture if is well-founded and extensional, and the field of either equals the downward closure of one of its members (called its top element), or is empty. Functions A functional relation is a binary predicate such that Such a relation (predicate) is implemented as a relation (set) exactly as described in the previous section. So the predicate is implemented by the set . A relation is a function if and only if It is therefore possible to define the value function as the unique object such that – i.e.: is -related to such that the relation holds between and – or as the unique object such that . The presence in both theories of functional predicates which are not sets makes it useful to allow the notation both for sets and for important functional predicates. As long as one does not quantify over functions in the latter sense, all such uses are in principle eliminable. Outside of formal set theory, we usually specify a function in terms of its domain and codomain, as in the phrase "Let be a function". The domain of a function is just its domain as a relation, but we have not yet defined the codomain of a function. To