0004 Order
Let $X$ be a nonempty set and $\preceq \subseteq X^2$ a relation on $X$.
We say that $\preceq$ is a partial order if it is reflexive, anti-symmetric, and transitive.
If $\preceq$ is a partial order then we say that $(X,\preceq)$ is a partially ordered set or just poset for short.
We often write that $X$ is a poset, leaving it implicit that it is actually the pair $(X,\preceq)$ which is a poset.
When we express that $a\preceq b$ verbally, we may say that "$a$ precedes or equals $b$". I personally shorten this to "$a$ left-eqs $b$".
The notation $a\succeq b$ is syntactic sugar for $b\preceq a$. To pronounce "$a \succeq b$" we may say "$a$ succeeds or equals $b$". Or for short, just "$a$ right-eqs $b$".
For any two elements $a,b\in X$, if neither $a\preceq b$ nor $b\preceq a$, then we say that $a$ and $b$ are incommensurable with respect to $\preceq$. Otherwise they are commensurable.
If every two elements of $X$ are commensurable, we say that $\preceq$ is total, or a total order on $X$. We also say that $(X,\preceq)$ is a totally ordered set.
If $\preceq$ is a partial order, then we define the relation $\prec\subseteq X^2$ by
$$ a\prec b \quad \Leftrightarrow \quad a \prec b, \text{ and } a\ne b, \quad \forall a,b\in X $$
To pronounce $a\prec b$ we say "$a$ precedes $b$". The expression $a\succ b$ is syntactic sugar for $b\prec a$ and we say that "$a$ succeeds $b$".
Throughout this section, assume that $(X,\preceq)$ is a poset.
Theorem: Poset prec. strict part. ord.
Precedence is a strict partial order.
Statement and proof.
Statement: The relation $\prec$ is a strict partial order on $X$, meaning that it is irreflexive, asymmetric, and transitive.
Proof: Let $a,b,c\in X$.
Irreflexive.
Since $a=a$ we must not have $a\prec a$ and therefore $a\not\prec a$.
Asymmetric.
Let $a\prec b$ and assume for contradiction that $b\prec a$.
The former entails $a\preceq b$ and the latter entails $b\preceq a$.
By the anti-symmetry of $\preceq$, then we have $a=b$.
But $a\prec b$ also implies $a\ne b$, a contradiction.
Transitive.
Suppose $a\prec b$ and $b\prec c$. Then $a\preceq b$ and $b\preceq c$, so by transitivity of $\preceq$ we have $a\preceq c$.
Assume for contradiction that $a=c$. Then $a\preceq b$ and $b\preceq a$ so $a=b$ by the anti-symmetry of $\preceq$.
But $a\prec b$ entails $a\ne b$, a contradiction.
$\Box$
Theorem: Poset neg. prec.
If $a\prec b$ then $b\not\preceq a$, and the converse if $\preceq$ is total.
Statement and proof.
Statement: If $a,b\in X$ are such that $a\prec b$ then $b\not\preceq a$.
Moreover, if $\preceq$ is a total order, then $b\not\preceq a$ entails $a\prec b$.
Proof: Suppose $a \prec b$. Then by the asymmetry of $\prec$ we have $b\not\prec a$ so either $b\not\preceq a$ or $b=a$.
But $a\prec b$ entails $a\ne b$, so it follows that $b\not\preceq a$.
Now assume that $\preceq$ is a total order, and $b\not\preceq a$. Then it follows that $a\preceq b$ by the totality property.
Moreover, if $a=b$ then we would have $b\preceq a$, so this cannot hold and therefore $a\ne b$.
This entails $a\prec b$.
$\Box$