Let X, Tx, C and D be given.
Assume Htop: topology_on X Tx.
Assume HC: closed_in X Tx C.
Assume HD: closed_in X Tx D.
We will prove closure_of X Tx (C ∩ D) = C ∩ D.
We prove the intermediate claim HCD_closed: closed_in X Tx (C ∩ D).
An exact proof term for the current goal is (intersection_of_closed_is_closed X Tx C D Htop HC HD).
We prove the intermediate claim HCD_sub: C ∩ D ⊆ X.
Let x be given.
Assume Hx: x ∈ C ∩ D.
We prove the intermediate claim HxC: x ∈ C.
An exact proof term for the current goal is (binintersectE1 C D x Hx).
We prove the intermediate claim HC_sub: C ⊆ X.
An exact proof term for the current goal is (andEL (C ⊆ X) (∃U ∈ Tx, C = X ∖ U) (andER (topology_on X Tx) (C ⊆ X ∧ ∃U ∈ Tx, C = X ∖ U) HC)).
An exact proof term for the current goal is (HC_sub x HxC).
Apply set_ext to the current goal.
Let x be given.
Assume Hx: x ∈ closure_of X Tx (C ∩ D).
We will prove x ∈ C ∩ D.
rewrite the current goal using (closed_closure_eq X Tx (C ∩ D) Htop HCD_closed) (from right to left).
An exact proof term for the current goal is Hx.
An exact proof term for the current goal is (subset_of_closure X Tx (C ∩ D) Htop HCD_sub).
∎