Partial and Total Orders on a Set and the Associated Strict Relation

In the setting of Class Theory NBG: the Axioms, Standing Conventions and Basic Notation, let $a$ be a set.

¶ A partial order on $a$ is a relation $\le$ on $a$ such that $\le$ is reflexive, antisymmetric and transitive; for sets $u$ and $v$, $u\le v$ means $(u,v)\in{\le}$, as in Relations, Domain, Range, Inverse and Composition §relation.

Throughout the remaining clauses, $\le$ is a partial order on $a$.

¶ The partial order $\le$ is total (a total order on $a$) if for all $u,v\in a$, $u\le v$ or $v\le u$.

¶ The strict relation associated with $\le$ is the class

$${<}=\{p:\exists u\,\exists v\,(p=(u,v)\wedge u\le v\wedge u\neq v)\},$$

formed by class abstraction with the class parameter $\le$; its formula quantifies over set variables only, the ordered pair $(u,v)$ being a defined set symbol, so it is predicative as Class Theory NBG: the Axioms, Standing Conventions and Basic Notation §comprehension requires. For sets $u$ and $v$, $u<v$ means $(u,v)\in{<}$.