For ordinals and let be the Order Type of (Disjoint Union of Well Ordered Sets) Proposition The Ordinal Addition (inductive) and synthetic definitions coincide.