Let alpha be given.

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

Let beta be given.

Assume H2: beta ∈ alpha.

We will prove TransSet beta ∧ ∀x ∈ beta, TransSet x.

Apply H1 to the current goal.

Assume H3: TransSet alpha.

Assume H4: ∀x ∈ alpha, TransSet x.

Apply andI to the current goal.

An exact proof term for the current goal is (H4 beta H2).

We will prove ∀x ∈ beta, TransSet x.

Let x be given.

Assume Hx: x ∈ beta.

We prove the intermediate claim L1: x ∈ alpha.

An exact proof term for the current goal is (H3 beta H2 x Hx).

We will prove TransSet x.

An exact proof term for the current goal is (H4 x L1).

∎