Let X, Tx, A and B be given.
Assume Htop: topology_on X Tx.
Assume HAB: A ⊆ B.
Assume HB: B ⊆ X.
We will prove closure_of X Tx A ⊆ closure_of X Tx B.
Let x be given.
Assume Hx: x ∈ closure_of X Tx A.
We will prove x ∈ 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 ≠ Empty) x Hx).
We prove the intermediate claim HcondA: ∀U : set, U ∈ Tx → x ∈ U → U ∩ A ≠ Empty.
An exact proof term for the current goal is (SepE2 X (λx0 ⇒ ∀U : set, U ∈ Tx → x0 ∈ U → U ∩ A ≠ Empty) x Hx).
We prove the intermediate claim HcondB: ∀U : set, U ∈ Tx → x ∈ U → U ∩ B ≠ Empty.
Let U be given.
Assume HU: U ∈ Tx.
Assume HxU: x ∈ U.
We will prove U ∩ B ≠ Empty.
We prove the intermediate claim HUA_ne: U ∩ A ≠ Empty.
An exact proof term for the current goal is (HcondA U HU HxU).
Assume Hempty: U ∩ B = Empty.
We prove the intermediate claim HUA_sub_UB: U ∩ A ⊆ U ∩ B.
Let y be given.
Assume Hy: y ∈ U ∩ A.
We prove the intermediate claim HyU: y ∈ U.
An exact proof term for the current goal is (binintersectE1 U A y Hy).
We prove the intermediate claim HyA: y ∈ A.
An exact proof term for the current goal is (binintersectE2 U A y Hy).
We prove the intermediate claim HyB: y ∈ B.
An exact proof term for the current goal is (HAB y HyA).
An exact proof term for the current goal is (binintersectI U B y HyU HyB).
We prove the intermediate claim HUA_empty: U ∩ A = Empty.
Apply Empty_Subq_eq to the current goal.
We prove the intermediate claim HUB_sub_Empty: U ∩ B ⊆ Empty.
rewrite the current goal using Hempty (from left to right).
An exact proof term for the current goal is (Subq_ref Empty).
An exact proof term for the current goal is (Subq_tra (U ∩ A) (U ∩ B) Empty HUA_sub_UB HUB_sub_Empty).
An exact proof term for the current goal is (HUA_ne HUA_empty).
An exact proof term for the current goal is (SepI X (λx0 ⇒ ∀U : set, U ∈ Tx → x0 ∈ U → U ∩ B ≠ Empty) x HxX HcondB).
∎