Let X and Y be given.

Apply set_ext to the current goal.

We will prove proj1 (pair X Y) ⊆ Y.

Let u be given.

Assume H1: u ∈ proj1 (pair X Y).

We will prove u ∈ Y.

Apply (pairE1 X Y u) to the current goal.

We will prove pair 1 u ∈ pair X Y.

An exact proof term for the current goal is (proj1E (pair X Y) u H1).

We will prove Y ⊆ proj1 (pair X Y).

Let u be given.

Assume H1: u ∈ Y.

We will prove u ∈ proj1 (pair X Y).

Apply proj1I to the current goal.

We will prove pair 1 u ∈ pair X Y.

Apply pairI1 to the current goal.

We will prove u ∈ Y.

An exact proof term for the current goal is H1.

∎