严格序

父节点：basic-orders

严格（偏）序

一个关系 <，满足非自反性（a < a 永不成立）和传递性。（非自反性 + 传递性已经蕴含了非对称性。）

它是 ≤ 的 < 侧影：从一个 partial-order ≤ 出发，令 a < b ⟺ a≤b ∧ a≠b；反过来，a ≤ b ⟺ a<b ∨ a=b。两种形式携带的是同一份信息。

严格全序额外满足三歧性：对任意 a,b，a<b、a=b、b<a 三者恰有一个成立。严格序是well-foundedness（"不存在无穷降链 … < a₂ < a₁"）的自然场景，因而也是序数与良基递归的自然场景。