Let X, Tx, A, U and x be given.
Assume HTx: topology_on X Tx.
Assume Hint0: interior_of X Tx A = Empty.
Assume HU: U ∈ Tx.
Assume HxU: x ∈ U.
We will prove ¬ (U ⊆ A).
Assume Hsub: U ⊆ A.
We prove the intermediate claim HxInt: x ∈ interior_of X Tx A.
An exact proof term for the current goal is (interior_of_contains_open_subset_point X Tx A U x HTx HU HxU Hsub).
We prove the intermediate claim HxEmpty: x ∈ Empty.
rewrite the current goal using Hint0 (from right to left).
An exact proof term for the current goal is HxInt.
An exact proof term for the current goal is ((EmptyE x) HxEmpty).
∎