Let X and Y be given.

Apply (binintersect_Subq_max Y X (X ∩ Y)) to the current goal.

We will prove X ∩ Y ⊆ Y.

Apply binintersect_Subq_2 to the current goal.

We will prove X ∩ Y ⊆ X.

Apply binintersect_Subq_1 to the current goal.

∎