Let X, Tx, A and B be given.

Assume Htop: topology_on X Tx.

Assume HAB: A ⊆ B.

We will prove interior_of X Tx A ⊆ interior_of X Tx B.

Let x be given.

Assume Hx: x ∈ interior_of X Tx A.

We will prove x ∈ interior_of X Tx B.

We prove the intermediate claim HxX: x ∈ X.

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

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_A: 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 HU: U ∈ Tx.

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

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).

We prove the intermediate claim HUsub_B: U ⊆ B.

An exact proof term for the current goal is (Subq_tra U A B HUsub_A HAB).

We prove the intermediate claim Hwitness: U ∈ Tx ∧ x ∈ U ∧ U ⊆ B.

Apply andI to the current goal.

An exact proof term for the current goal is HU.

An exact proof term for the current goal is HxU.

An exact proof term for the current goal is HUsub_B.

We prove the intermediate claim Hexists_B: ∃V : set, V ∈ Tx ∧ x ∈ V ∧ V ⊆ B.

We use U to witness the existential quantifier.

An exact proof term for the current goal is Hwitness.

An exact proof term for the current goal is (SepI X (λx0 ⇒ ∃V : set, V ∈ Tx ∧ x0 ∈ V ∧ V ⊆ B) x HxX Hexists_B).

∎