| context | $X$ |
| definiendum | $ <\ \in\ \text{StrictPartOrd}(X) $ |
| context | $ <\ \in\ \mathrm{Rel}(X) $ |
| $ x,y,z\in X $ |
| postulate | $ x \nless x $ |
| postulate | $ x<y\land y<z \implies x<z $ |
Here we use infix notation: $x<y\ \equiv\ <(x,y)$.
A strict partial order is automatically anti-symmetric.
Wikipedia: Order theory, Poset