Let X, Tx, A and B be given.

Assume Htop: topology_on X Tx.

Assume HA: A ⊆ X.

Assume HB: B ⊆ X.

We will prove interior_of X Tx A ∪ interior_of X Tx B ⊆ interior_of X Tx (A ∪ B).

We prove the intermediate claim HAB_union_A: A ⊆ A ∪ B.

Let x be given.

Assume Hx: x ∈ A.

An exact proof term for the current goal is (binunionI1 A B x Hx).

We prove the intermediate claim HAB_union_B: B ⊆ A ∪ B.

Let x be given.

Assume Hx: x ∈ B.

An exact proof term for the current goal is (binunionI2 A B x Hx).

We prove the intermediate claim HAB_sub: A ∪ B ⊆ X.

Let x be given.

Assume Hx: x ∈ A ∪ B.

Apply (binunionE A B x Hx) to the current goal.

Assume HxA: x ∈ A.

An exact proof term for the current goal is (HA x HxA).

Assume HxB: x ∈ B.

An exact proof term for the current goal is (HB x HxB).

We prove the intermediate claim HintA: interior_of X Tx A ⊆ interior_of X Tx (A ∪ B).

An exact proof term for the current goal is (interior_monotone X Tx A (A ∪ B) Htop HAB_union_A).

We prove the intermediate claim HintB: interior_of X Tx B ⊆ interior_of X Tx (A ∪ B).

An exact proof term for the current goal is (interior_monotone X Tx B (A ∪ B) Htop HAB_union_B).

Let x be given.

Assume Hx: x ∈ interior_of X Tx A ∪ interior_of X Tx B.

Apply (binunionE (interior_of X Tx A) (interior_of X Tx B) x Hx) to the current goal.

Assume HxA: x ∈ interior_of X Tx A.

An exact proof term for the current goal is (HintA x HxA).

Assume HxB: x ∈ interior_of X Tx B.

An exact proof term for the current goal is (HintB x HxB).

∎