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 closure_of X Tx (A ∩ B) ⊆ closure_of X Tx A ∩ closure_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 HAB_X: A ∩ B ⊆ X.
Let x be given.
Assume Hx: x ∈ A ∩ B.
An exact proof term for the current goal is (HA x (binintersectE1 A B x Hx)).
We prove the intermediate claim HclAB_A: closure_of X Tx (A ∩ B) ⊆ closure_of X Tx A.
An exact proof term for the current goal is (closure_monotone X Tx (A ∩ B) A Htop HAB_A HA).
We prove the intermediate claim HclAB_B: closure_of X Tx (A ∩ B) ⊆ closure_of X Tx B.
An exact proof term for the current goal is (closure_monotone X Tx (A ∩ B) B Htop HAB_B HB).
Let x be given.
Assume Hx: x ∈ closure_of X Tx (A ∩ B).
Apply binintersectI to the current goal.
An exact proof term for the current goal is (HclAB_A x Hx).
An exact proof term for the current goal is (HclAB_B x Hx).
∎