Let alpha and beta be given.

Assume H1: ordinal alpha.

Assume H2: ordinal beta.

Apply (or3E (alpha ∈ beta) (alpha = beta) (beta ∈ alpha) (ordinal_trichotomy_or alpha beta H1 H2)) to the current goal.

Assume H3: alpha ∈ beta.

Apply orIL to the current goal.

An exact proof term for the current goal is H3.

Assume H3: alpha = beta.

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: beta ∈ alpha.

Apply orIR to the current goal.

An exact proof term for the current goal is (ordinal_TransSet alpha H1 beta H3).

∎