Let X be given.

Assume H1: TransSet X.

Let x be given.

Assume H2: x ∈ X.

Let y be given.

Assume H3: y ∈ ordsucc x.

We will prove y ∈ X.

Apply (ordsuccE x y H3) to the current goal.

Assume H4: y ∈ x.

An exact proof term for the current goal is (H1 x H2 y H4).

Assume H4: y = x.

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

We will prove x ∈ X.

An exact proof term for the current goal is H2.

∎