Let α be given.

Assume H: ordinal α.

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

∎