Let alpha be given.

Assume H1: TransSet alpha ∧ ∀beta ∈ alpha, TransSet beta.

Apply H1 to the current goal.

Assume H2: TransSet alpha.

Assume H3: ∀beta ∈ alpha, TransSet beta.

We will prove TransSet (ordsucc alpha) ∧ ∀beta ∈ ordsucc alpha, TransSet beta.

Apply andI to the current goal.

An exact proof term for the current goal is (TransSet_ordsucc alpha H2).

Let beta be given.

Assume H4: beta ∈ ordsucc alpha.

We will prove TransSet beta.

Apply (ordsuccE alpha beta H4) to the current goal.

Assume H5: beta ∈ alpha.

An exact proof term for the current goal is (H3 beta H5).

Assume H5: beta = alpha.

rewrite the current goal using H5 (from left to right).

An exact proof term for the current goal is H2.

∎