Let X be given.

Assume H1: TransSet X.

Let x be given.

Assume H2: x ∈ ordsucc X.

Let y be given.

Assume H3: y ∈ x.

We will prove y ∈ ordsucc X.

Apply (ordsuccE X x H2) to the current goal.

Assume H4: x ∈ X.

Apply ordsuccI1 to the current goal.

We will prove y ∈ X.

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

Assume H4: x = X.

Apply ordsuccI1 to the current goal.

We will prove y ∈ X.

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

We will prove y ∈ x.

An exact proof term for the current goal is H3.

∎