Let α be given.

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

Let β be given.

Assume H2: β ∈ α.

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

Apply H1 to the current goal.

Assume H3: TransSet α.

Assume H4: ∀x ∈ α, TransSet x.

Apply andI to the current goal.

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

We will prove ∀x ∈ β, TransSet x.

Let x be given.

Assume Hx: x ∈ β.

We prove the intermediate claim L1: x ∈ α.

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

We will prove TransSet x.

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

∎