Let X, Tx and A be given.

Assume Htop: topology_on X Tx.

We will prove interior_of X Tx A ⊆ A.

Let x be given.

Assume Hx: x ∈ interior_of X Tx A.

We will prove x ∈ A.

We prove the intermediate claim Hexists: ∃U : set, U ∈ Tx ∧ x ∈ U ∧ U ⊆ A.

An exact proof term for the current goal is (SepE2 X (λx0 ⇒ ∃U : set, U ∈ Tx ∧ x0 ∈ U ∧ U ⊆ A) x Hx).

Apply Hexists to the current goal.

Let U be given.

Assume HU_conj: U ∈ Tx ∧ x ∈ U ∧ U ⊆ A.

We prove the intermediate claim HU_and_x: U ∈ Tx ∧ x ∈ U.

An exact proof term for the current goal is (andEL (U ∈ Tx ∧ x ∈ U) (U ⊆ A) HU_conj).

We prove the intermediate claim HUsub: U ⊆ A.

An exact proof term for the current goal is (andER (U ∈ Tx ∧ x ∈ U) (U ⊆ A) HU_conj).

We prove the intermediate claim HxU: x ∈ U.

An exact proof term for the current goal is (andER (U ∈ Tx) (x ∈ U) HU_and_x).

An exact proof term for the current goal is (HUsub x HxU).

∎