Let X, Tx and A be given.

Assume Htop: topology_on X Tx.

Assume HA: A ⊆ X.

We will prove interior_of X Tx (interior_of X Tx A) = interior_of X Tx A.

We prove the intermediate claim HintA_open: interior_of X Tx A ∈ Tx.

An exact proof term for the current goal is (interior_is_open X Tx A Htop HA).

An exact proof term for the current goal is (open_interior_eq X Tx (interior_of X Tx A) Htop HintA_open).

∎