Definition 1.4.24 (Succession).  Let S, T be sets, ⪯ be a partial order on S, ⊑ be a partial order on T. We define:
⪯ ≪ ⊑ := [{[{sa ⪯ sb if a = l(sa) (sa ∈ S)false if a = r(ta) (ta ∈ T)] if b = l(sb) (sb ∈ S)[{true if a = l(sa) (sa ∈ S)ta ⊑ tb if a = r(ta) (ta ∈ T)] if b = r(tb) (tb ∈ T)]a,b ∈ S ⊎ T
Remarks.

This definition constructs a partial order on the disjoint union of two sets S and T from partial orders on S and T. Elements of S are always considered smaller than elements of T. This is used to define addition of ordinal numbers (see $../Numbers/Ordinal/sum).

References.