Let X, Tx, A and B be given.
Assume Htop: topology_on X Tx.
We will prove closure_of X Tx (A ∩ B) ⊆ closure_of X Tx A ∩ closure_of X Tx B.
Let x be given.
Assume Hx: x ∈ closure_of X Tx (A ∩ B).
We will prove x ∈ closure_of X Tx A ∩ closure_of X Tx B.
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (SepE1 X (λx0 ⇒ ∀U : set, U ∈ Tx → x0 ∈ U → U ∩ (A ∩ B) ≠ Empty) x Hx).
We prove the intermediate claim HxAB: ∀U : set, U ∈ Tx → x ∈ U → U ∩ (A ∩ B) ≠ Empty.
An exact proof term for the current goal is (SepE2 X (λx0 ⇒ ∀U : set, U ∈ Tx → x0 ∈ U → U ∩ (A ∩ B) ≠ Empty) x Hx).
Apply binintersectI to the current goal.
We will prove x ∈ closure_of X Tx A.
We prove the intermediate claim HxA: x ∈ X ∧ (∀U : set, U ∈ Tx → x ∈ U → U ∩ A ≠ Empty).
Apply andI to the current goal.
An exact proof term for the current goal is HxX.
Let U be given.
Assume HU: U ∈ Tx.
Assume HxU: x ∈ U.
We will prove U ∩ A ≠ Empty.
We prove the intermediate claim HABne: U ∩ (A ∩ B) ≠ Empty.
An exact proof term for the current goal is (HxAB U HU HxU).
Assume Hempty: U ∩ A = Empty.
Apply HABne to the current goal.
Apply Empty_Subq_eq to the current goal.
Let y be given.
Assume Hy: y ∈ U ∩ (A ∩ B).
We prove the intermediate claim HyU: y ∈ U.
An exact proof term for the current goal is (binintersectE1 U (A ∩ B) y Hy).
We prove the intermediate claim HyAB: y ∈ A ∩ B.
An exact proof term for the current goal is (binintersectE2 U (A ∩ B) y Hy).
We prove the intermediate claim HyA: y ∈ A.
An exact proof term for the current goal is (binintersectE1 A B y HyAB).
We prove the intermediate claim HyUA: y ∈ U ∩ A.
Apply binintersectI to the current goal.
An exact proof term for the current goal is HyU.
An exact proof term for the current goal is HyA.
rewrite the current goal using Hempty (from right to left).
An exact proof term for the current goal is HyUA.
An exact proof term for the current goal is (SepI X (λx0 ⇒ ∀U : set, U ∈ Tx → x0 ∈ U → U ∩ A ≠ Empty) x HxX (andER (x ∈ X) (∀U : set, U ∈ Tx → x ∈ U → U ∩ A ≠ Empty) HxA)).
We will prove x ∈ closure_of X Tx B.
We prove the intermediate claim HxB: x ∈ X ∧ (∀U : set, U ∈ Tx → x ∈ U → U ∩ B ≠ Empty).
Apply andI to the current goal.
An exact proof term for the current goal is HxX.
Let U be given.
Assume HU: U ∈ Tx.
Assume HxU: x ∈ U.
We will prove U ∩ B ≠ Empty.
We prove the intermediate claim HABne: U ∩ (A ∩ B) ≠ Empty.
An exact proof term for the current goal is (HxAB U HU HxU).
Assume Hempty: U ∩ B = Empty.
Apply HABne to the current goal.
Apply Empty_Subq_eq to the current goal.
Let y be given.
Assume Hy: y ∈ U ∩ (A ∩ B).
We prove the intermediate claim HyU: y ∈ U.
An exact proof term for the current goal is (binintersectE1 U (A ∩ B) y Hy).
We prove the intermediate claim HyAB: y ∈ A ∩ B.
An exact proof term for the current goal is (binintersectE2 U (A ∩ B) y Hy).
We prove the intermediate claim HyB: y ∈ B.
An exact proof term for the current goal is (binintersectE2 A B y HyAB).
We prove the intermediate claim HyUB: y ∈ U ∩ B.
Apply binintersectI to the current goal.
An exact proof term for the current goal is HyU.
An exact proof term for the current goal is HyB.
rewrite the current goal using Hempty (from right to left).
An exact proof term for the current goal is HyUB.
An exact proof term for the current goal is (SepI X (λx0 ⇒ ∀U : set, U ∈ Tx → x0 ∈ U → U ∩ B ≠ Empty) x HxX (andER (x ∈ X) (∀U : set, U ∈ Tx → x ∈ U → U ∩ B ≠ Empty) HxB)).
∎