Let X, Tx, U and A be given.
Assume Htop: topology_on X Tx.
Assume HUopen: U ∈ Tx.
Assume HUsubA: U ⊆ A.
Assume Hint: interior_of X Tx A = Empty.
We will prove U = Empty.
Apply set_ext to the current goal.
We will prove U ⊆ Empty.
Let x be given.
Assume HxU: x ∈ U.
We will prove x ∈ Empty.
We prove the intermediate claim Hxint: x ∈ interior_of X Tx A.
An exact proof term for the current goal is (open_subset_interior X Tx U A Htop HUopen HUsubA x HxU).
rewrite the current goal using Hint (from right to left).
An exact proof term for the current goal is Hxint.
An exact proof term for the current goal is (Subq_Empty U).
∎