Let alpha and beta be given.

Assume H1: ordinal alpha.

Assume H2: ordinal beta.

Apply (ordinal_In_Or_Subq 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 (ordinal_TransSet beta H2 alpha H3).

Assume H3: beta ⊆ alpha.

Apply orIR to the current goal.

An exact proof term for the current goal is H3.

∎