Let J, a and b be given.

Assume Hab: (a,b) ∈ inclusion_rel J.

We prove the intermediate claim Hab': (a,b) ∈ {p ∈ setprod J J|(p 0) ⊆ (p 1)}.

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

An exact proof term for the current goal is Hab.

We prove the intermediate claim Hprod: (a,b) ∈ setprod J J.

An exact proof term for the current goal is (SepE1 (setprod J J) (λp : set ⇒ (p 0) ⊆ (p 1)) (a,b) Hab').

We prove the intermediate claim Hsub: (a,b) 0 ⊆ (a,b) 1.

An exact proof term for the current goal is (SepE2 (setprod J J) (λp : set ⇒ (p 0) ⊆ (p 1)) (a,b) Hab').

Apply andI to the current goal.

An exact proof term for the current goal is Hprod.

We will prove a ⊆ b.

Let y be given.

Assume Hy: y ∈ a.

We will prove y ∈ b.

We prove the intermediate claim Hy0: y ∈ (a,b) 0.

rewrite the current goal using (tuple_2_0_eq a b) (from left to right).

An exact proof term for the current goal is Hy.

We prove the intermediate claim Hy1: y ∈ (a,b) 1.

An exact proof term for the current goal is (Hsub y Hy0).

rewrite the current goal using (tuple_2_1_eq a b) (from right to left).

An exact proof term for the current goal is Hy1.

∎