Let X, Tx, A and C be given.
Assume Htop: topology_on X Tx.
Assume HAC: A ⊆ C.
Assume HC: closed_in X Tx C.
We will prove closure_of X Tx A ⊆ C.
Let x be given.
Assume Hx: x ∈ closure_of X Tx A.
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 HCparts: 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 HxX: x ∈ X.
An exact proof term for the current goal is (closure_in_space X Tx A Htop 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).
Apply (andER (C ⊆ X) (∃U ∈ Tx, C = X ∖ U) HCparts) to the current goal.
Let U be given.
Assume HUconj: 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) HUconj).
We prove the intermediate claim HCeq: C = X ∖ U.
An exact proof term for the current goal is (andER (U ∈ Tx) (C = X ∖ U) HUconj).
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 FalseE to the current goal.
Apply HxnotC to the current goal.
We prove the intermediate claim HxXU: x ∈ X ∖ U.
An exact proof term for the current goal is (setminusI X U x HxX 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 HUAne: U ∩ A ≠ Empty.
An exact proof term for the current goal is (HcondA U HU HxU).
We prove the intermediate claim HUAempty: U ∩ A = Empty.
Apply Empty_Subq_eq to the current goal.
Let y be given.
Assume Hy: y ∈ U ∩ A.
We will prove y ∈ Empty.
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 HyC: y ∈ C.
An exact proof term for the current goal is (HAC y HyA).
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).
Apply FalseE to the current goal.
An exact proof term for the current goal is (HUAne HUAempty).
∎