Let X, T1, T2 and A be given.

Assume Hfin: finer_than T1 T2.

We will prove closure_of X T1 A ⊆ closure_of X T2 A.

Let x be given.

Assume Hx: x ∈ closure_of X T1 A.

We will prove x ∈ closure_of X T2 A.

We prove the intermediate claim HxX: x ∈ X.

An exact proof term for the current goal is (SepE1 X (λx0 : set ⇒ ∀U : set, U ∈ T1 → x0 ∈ U → U ∩ A ≠ Empty) x Hx).

We prove the intermediate claim Hcond: ∀U : set, U ∈ T1 → x ∈ U → U ∩ A ≠ Empty.

An exact proof term for the current goal is (SepE2 X (λx0 : set ⇒ ∀U : set, U ∈ T1 → x0 ∈ U → U ∩ A ≠ Empty) x Hx).

We prove the intermediate claim Hcond2: ∀U : set, U ∈ T2 → x ∈ U → U ∩ A ≠ Empty.

Let U be given.

Assume HU2: U ∈ T2.

Assume HxU: x ∈ U.

We will prove U ∩ A ≠ Empty.

We prove the intermediate claim HU1: U ∈ T1.

An exact proof term for the current goal is (Hfin U HU2).

An exact proof term for the current goal is (Hcond U HU1 HxU).

An exact proof term for the current goal is (SepI X (λx0 : set ⇒ ∀U : set, U ∈ T2 → x0 ∈ U → U ∩ A ≠ Empty) x HxX Hcond2).

∎