Let alpha be given.

Assume H: ordinal alpha.

An exact proof term for the current goal is (TransSet_ordsucc_In_Subq alpha (ordinal_TransSet alpha H)).

∎