Let X, Tx and C be given.
Assume Htop: topology_on X Tx.
Assume HC: closed_in X Tx C.
We will prove closure_of X Tx C = C.
We prove the intermediate claim HTx: topology_on X Tx.
An exact proof term for the current goal is (andEL (topology_on X Tx) (C ⊆ X ∧ ∃U ∈ Tx, C = X ∖ U) HC).
We prove the intermediate claim HCsub_and_ex: C ⊆ X ∧ ∃U ∈ Tx, C = X ∖ U.
An exact proof term for the current goal is (andER (topology_on X Tx) (C ⊆ X ∧ ∃U ∈ Tx, C = X ∖ U) HC).
We prove the intermediate claim HCsub: C ⊆ X.
An exact proof term for the current goal is (andEL (C ⊆ X) (∃U ∈ Tx, C = X ∖ U) HCsub_and_ex).
Apply set_ext to the current goal.
We will prove closure_of X Tx C ⊆ C.
Let x be given.
Assume Hx: x ∈ closure_of X Tx C.
We will prove x ∈ C.
Apply (xm (x ∈ C)) to the current goal.
Assume HxC: x ∈ C.
An exact proof term for the current goal is HxC.
Assume HxnotC: x ∉ C.
We prove the intermediate claim Hex: ∃U ∈ Tx, C = X ∖ U.
An exact proof term for the current goal is (andER (C ⊆ X) (∃U ∈ Tx, C = X ∖ U) HCsub_and_ex).
Apply Hex to the current goal.
Let U be given.
Assume HU_conj: U ∈ Tx ∧ C = X ∖ U.
We prove the intermediate claim HU: U ∈ Tx.
An exact proof term for the current goal is (andEL (U ∈ Tx) (C = X ∖ U) HU_conj).
We prove the intermediate claim HCeq: C = X ∖ U.
An exact proof term for the current goal is (andER (U ∈ Tx) (C = X ∖ U) HU_conj).
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (closure_in_space X Tx C Htop x Hx).
We prove the intermediate claim Hcond: ∀V : set, V ∈ Tx → x ∈ V → V ∩ C ≠ Empty.
An exact proof term for the current goal is (SepE2 X (λx0 ⇒ ∀V : set, V ∈ Tx → x0 ∈ V → V ∩ C ≠ Empty) x Hx).
We prove the intermediate claim HxU: x ∈ U.
Apply (xm (x ∈ U)) to the current goal.
Assume H.
An exact proof term for the current goal is H.
Assume HxnotU: x ∉ U.
Apply HxnotC to the current goal.
We prove the intermediate claim HxXU: x ∈ X ∖ U.
Apply setminusI to the current goal.
An exact proof term for the current goal is HxX.
An exact proof term for the current goal is HxnotU.
rewrite the current goal using HCeq (from left to right).
An exact proof term for the current goal is HxXU.
We prove the intermediate claim HUC_ne: U ∩ C ≠ Empty.
An exact proof term for the current goal is (Hcond U HU HxU).
We prove the intermediate claim HUC_empty: U ∩ C = Empty.
Apply set_ext to the current goal.
Let y be given.
Assume Hy: y ∈ U ∩ C.
We will prove y ∈ Empty.
We prove the intermediate claim HyU: y ∈ U.
An exact proof term for the current goal is (binintersectE1 U C y Hy).
We prove the intermediate claim HyC: y ∈ C.
An exact proof term for the current goal is (binintersectE2 U C y Hy).
We prove the intermediate claim HyXU: y ∈ X ∖ U.
rewrite the current goal using HCeq (from right to left).
An exact proof term for the current goal is HyC.
We prove the intermediate claim HynotU: y ∉ U.
An exact proof term for the current goal is (setminusE2 X U y HyXU).
Apply FalseE to the current goal.
An exact proof term for the current goal is (HynotU HyU).
An exact proof term for the current goal is (Subq_Empty (U ∩ C)).
Apply FalseE to the current goal.
An exact proof term for the current goal is (HUC_ne HUC_empty).
An exact proof term for the current goal is (subset_of_closure X Tx C Htop HCsub).
∎