total_order

Total order

context

$X$

definiendum

$\le\ \in\ \mathrm{it}$

The relation $\le$ is an order relation if it's in the intersection of all total, all anti-symmetric and all transitive relation. Hence

context	$\le\ \in\ \mathrm{Rel}(X)$
$x,y,z \in X$

postulate	$x \le y\ \lor\ y \le x$
postulate	$x\le y\ \land\ y\le x \implies (x=y)$
postulate	$x \le y\ \land\ y \le z \Leftrightarrow x\le z$