Let α and β be given.

Assume H1: ordinal α.

Assume H2: ordinal β.

Apply (ordinal_In_Or_Subq α β H1 H2) to the current goal.

Assume H3: α ∈ β.

Apply orIL to the current goal.

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

Assume H3: β ⊆ α.

Apply orIR to the current goal.

An exact proof term for the current goal is H3.

∎