Let X, T and C be given.
Assume HC: closed_in X T C.
We will prove open_in X T (X ∖ C).
We prove the intermediate claim HTx: topology_on X T.
An exact proof term for the current goal is (closed_in_topology X T C HC).
We prove the intermediate claim HCex: ∃U ∈ T, C = X ∖ U.
An exact proof term for the current goal is (closed_in_exists_open_complement X T C HC).
Apply HCex to the current goal.
Let U be given.
Assume HU: U ∈ T ∧ C = X ∖ U.
We prove the intermediate claim HUinT: U ∈ T.
An exact proof term for the current goal is (andEL (U ∈ T) (C = X ∖ U) HU).
We prove the intermediate claim HCeq: C = X ∖ U.
An exact proof term for the current goal is (andER (U ∈ T) (C = X ∖ U) HU).
We prove the intermediate claim HUsubX: U ⊆ X.
An exact proof term for the current goal is (topology_elem_subset X T U HTx HUinT).
We prove the intermediate claim HXCe: X ∖ C = U.
rewrite the current goal using HCeq (from left to right).
We will prove X ∖ (X ∖ U) = U.
Apply set_ext to the current goal.
Let x be given.
Assume Hx: x ∈ X ∖ (X ∖ U).
We will prove x ∈ U.
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (setminusE1 X (X ∖ U) x Hx).
We prove the intermediate claim HxnotXU: x ∉ X ∖ U.
An exact proof term for the current goal is (setminusE2 X (X ∖ U) x Hx).
Apply (xm (x ∈ U)) to the current goal.
Assume HxU: x ∈ U.
An exact proof term for the current goal is HxU.
Assume HxnotU: x ∉ U.
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.
Apply FalseE to the current goal.
An exact proof term for the current goal is (HxnotXU HxXU).
Let x be given.
Assume Hx: x ∈ U.
We will prove x ∈ X ∖ (X ∖ U).
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (HUsubX x Hx).
Apply setminusI to the current goal.
An exact proof term for the current goal is HxX.
Assume HxXU: x ∈ X ∖ U.
We prove the intermediate claim HxnotU: x ∉ U.
An exact proof term for the current goal is (setminusE2 X U x HxXU).
An exact proof term for the current goal is (HxnotU Hx).
Apply (open_inI X T (X ∖ C) HTx) to the current goal.
rewrite the current goal using HXCe (from left to right).
An exact proof term for the current goal is HUinT.
∎