Let X and T be given.
Assume HTx: topology_on X T.
We will prove closed_in X T X.
Apply (closed_inI X T X) to the current goal.
An exact proof term for the current goal is HTx.
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 T HTx).
We will prove X = X ∖ Empty.
Apply set_ext to the current goal.
Let x be given.
Assume Hx: x ∈ X.
We will prove x ∈ X ∖ Empty.
Apply setminusI to the current goal.
An exact proof term for the current goal is Hx.
Assume H: x ∈ Empty.
An exact proof term for the current goal is (EmptyE x H).
Let x be given.
Assume Hx: x ∈ X ∖ Empty.
An exact proof term for the current goal is (setminusE1 X Empty x Hx).
∎