Let X be given.
We will prove closure_of X (discrete_topology X) (X ∖ Empty) = X.
We prove the intermediate claim Htop: topology_on X (discrete_topology X).
An exact proof term for the current goal is (discrete_topology_on X).
We prove the intermediate claim HXE: X ∖ Empty = X.
Apply set_ext to the current goal.
Let x be given.
Assume Hx: x ∈ X ∖ Empty.
An exact proof term for the current goal is (setminusE1 X Empty x Hx).
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 Hfalse: x ∈ Empty.
An exact proof term for the current goal is (EmptyE x Hfalse).
rewrite the current goal using HXE (from left to right).
Apply set_ext to the current goal.
An exact proof term for the current goal is (closure_in_space X (discrete_topology X) X Htop).
An exact proof term for the current goal is (subset_of_closure X (discrete_topology X) X Htop (Subq_ref X)).
∎