Partial Order

DEF-PO. Partial Order.

• A partial order is an antisymmetric preorder, i.e. a binary relation that is reflexive, transitive and antisymmetric.

• A strict partial order is a binary relation that is irreflexive, transitive and asymmetric.

PROP-PO-ASY.

A relation is a strict partial order as soon as it is irreflexive and transitive.

Proof.By PROP-RCL-ITA.

PROP-PO-S.

$\preceq$ is a partial order if and only if $\prec$ is a strict partial order.