Check that Prd methods are internally consistent.

This is a required property.

\( \forall a, b: (a = b) \Leftrightarrow (b = a) \)

=~ is a symmetric relation.

This is a required property.

\( \forall a: (a = a) \)

=~ is a reflexive relation.

This is a required property.

\( \forall a, b, c: ((a = b) \wedge (b = c)) \Rightarrow (a = c) \)

=~ is a transitive relation.

This is a required property.

\( \forall a, b: (a \leq b) \wedge (b \leq a) \Rightarrow a = b \)

<= is an antisymmetric relation.

This is a required property.

\( \forall a: (a \leq a) \)

<= is a reflexive relation.

This is a required property.

\( \forall a, b, c: ((a \leq b) \wedge (b \leq c)) \Rightarrow (a \leq c) \)

<= is an transitive relation.

This is a required property.

\( \forall a, b: ((a \leq b) \vee (b \leq a)) \)

<= is a connex relation.

\( \forall a, b: (a \lt b) \Rightarrow \neg (b \lt a) \)

lt is an asymmetric relation.

This is a required property.

\( \forall a, b, c: ((a \lt b) \wedge (b \lt c)) \Rightarrow (a \lt c) \)

lt is a transitive relation.

This is a required property.

\( \forall a: \neg (a \lt a) \)

lt is an irreflexive relation.

This is a required property.

\( \forall a, b: \neg (a = b) \Rightarrow ((a \lt b) \vee (b \lt a)) \)

lt is a semiconnex relation.

\( \forall a, b, c: ((a \lt b) \vee (a = b) \vee (b \lt a)) \wedge \neg ((a \lt b) \wedge (a = b) \wedge (b \lt a)) \)

In other words, exactly one of \(a \lt b\), \(a = b\), or \(b \lt a\) holds.

If lt is a trichotomous relation then the set is totally ordered.

\( \forall x, y, z, w: x \lt y \wedge y \sim z \wedge z \lt w \Rightarrow x \lt w \)

A semiorder does not allow 2-2 chains.