Let X and Tx be given.
Assume Htop: topology_on X Tx.
We will prove closed_in X Tx X.
We will prove topology_on X Tx ∧ (X ⊆ X ∧ ∃U ∈ Tx, X = X ∖ U).
Apply andI to the current goal.
An exact proof term for the current goal is Htop.
Apply andI to the current goal.
An exact proof term for the current goal is (Subq_ref X).
We use Empty to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is (topology_has_empty X Tx Htop).
We will prove X = X ∖ Empty.
Apply set_ext to the current goal.
Let x be given.
Assume Hx: x ∈ X.
Apply setminusI to the current goal.
An exact proof term for the current goal is Hx.
Assume Hcontra: x ∈ Empty.
An exact proof term for the current goal is (EmptyE x Hcontra False).
Let x be given.
Assume Hx: x ∈ X ∖ Empty.
An exact proof term for the current goal is (setminusE1 X Empty x Hx).
∎