Let X, Tx, A and B be given.
Assume Htop: topology_on X Tx.
Assume HA: A ⊆ X.
Assume HB: B ⊆ X.
We will prove interior_of X Tx (A ∩ B) ⊆ interior_of X Tx A ∩ interior_of X Tx B.
We prove the intermediate claim HAB_A: A ∩ B ⊆ A.
An exact proof term for the current goal is (binintersect_Subq_1 A B).
We prove the intermediate claim HAB_B: A ∩ B ⊆ B.
An exact proof term for the current goal is (binintersect_Subq_2 A B).
We prove the intermediate claim HintAB_A: interior_of X Tx (A ∩ B) ⊆ interior_of X Tx A.
An exact proof term for the current goal is (interior_monotone X Tx (A ∩ B) A Htop HAB_A).
We prove the intermediate claim HintAB_B: interior_of X Tx (A ∩ B) ⊆ interior_of X Tx B.
An exact proof term for the current goal is (interior_monotone X Tx (A ∩ B) B Htop HAB_B).
Let x be given.
Assume Hx: x ∈ interior_of X Tx (A ∩ B).
Apply binintersectI to the current goal.
An exact proof term for the current goal is (HintAB_A x Hx).
An exact proof term for the current goal is (HintAB_B x Hx).
∎