Let X, Tx and Fam be given.
Assume Htop: topology_on X Tx.
Assume HFsub: ∀A : set, A ∈ Fam → A ⊆ X.
We will prove closure_of X Tx (intersection_of_family X Fam) ⊆ intersection_of_family X {closure_of X Tx A|A ∈ Fam}.
Set Aint to be the term intersection_of_family X Fam.
Set ClFam to be the term {closure_of X Tx A|A ∈ Fam}.
We prove the intermediate claim HAintSubX: Aint ⊆ X.
Let x be given.
Assume Hx: x ∈ Aint.
An exact proof term for the current goal is (SepE1 X (λx0 ⇒ ∀U : set, U ∈ Fam → x0 ∈ U) x Hx).
Let x be given.
Assume Hx: x ∈ closure_of X Tx Aint.
We will prove x ∈ intersection_of_family X ClFam.
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 ∩ Aint ≠ Empty) x Hx).
We prove the intermediate claim Hdef: intersection_of_family X ClFam = {x0 ∈ X|∀U : set, U ∈ ClFam → x0 ∈ U}.
Use reflexivity.
rewrite the current goal using Hdef (from left to right).
Apply SepI to the current goal.
An exact proof term for the current goal is HxX.
Let W be given.
Assume HW: W ∈ ClFam.
We will prove x ∈ W.
Apply (ReplE Fam (λA : set ⇒ closure_of X Tx A) W HW) to the current goal.
Let A be given.
Assume HAconj.
We prove the intermediate claim HAFam: A ∈ Fam.
An exact proof term for the current goal is (andEL (A ∈ Fam) (W = closure_of X Tx A) HAconj).
We prove the intermediate claim HWeq: W = closure_of X Tx A.
An exact proof term for the current goal is (andER (A ∈ Fam) (W = closure_of X Tx A) HAconj).
We prove the intermediate claim HAintSubA: Aint ⊆ A.
Let y be given.
Assume Hy: y ∈ Aint.
We prove the intermediate claim Hcond: ∀U : set, U ∈ Fam → y ∈ U.
An exact proof term for the current goal is (SepE2 X (λx0 ⇒ ∀U : set, U ∈ Fam → x0 ∈ U) y Hy).
An exact proof term for the current goal is (Hcond A HAFam).
We prove the intermediate claim HxclA: x ∈ closure_of X Tx A.
An exact proof term for the current goal is (closure_monotone X Tx Aint A Htop HAintSubA (HFsub A HAFam) x Hx).
rewrite the current goal using HWeq (from left to right).
An exact proof term for the current goal is HxclA.
∎