Let α and β be given.

Assume H1: ordinal α.

Assume H2: ordinal β.

Apply (or3E (α ∈ β) (α = β) (β ∈ α) (ordinal_trichotomy_or α β H1 H2)) to the current goal.

Assume H3: α ∈ β.

Apply orIL to the current goal.

An exact proof term for the current goal is H3.

Assume H3: α = β.

Apply orIR to the current goal.

rewrite the current goal using H3 (from left to right).

Apply Subq_ref to the current goal.

Assume H3: β ∈ α.

Apply orIR to the current goal.

An exact proof term for the current goal is (ordinal_TransSet α H1 β H3).

∎