Let X, Y and Z be given.

Assume H1: Z ⊆ X.

Assume H2: Z ⊆ Y.

Let w be given.

Assume H3: w ∈ Z.

Apply (binintersectI X Y w) to the current goal.

We will prove w ∈ X.

An exact proof term for the current goal is (H1 w H3).

We will prove w ∈ Y.

An exact proof term for the current goal is (H2 w H3).

∎