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 closure_of X Tx A ∪ closure_of X Tx B ⊆ closure_of X Tx (A ∪ B).

We prove the intermediate claim HAB_union: 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 HBB_union: 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 HclA: closure_of X Tx A ⊆ closure_of X Tx (A ∪ B).

An exact proof term for the current goal is (closure_monotone X Tx A (A ∪ B) Htop HAB_union HAB_sub).

We prove the intermediate claim HclB: closure_of X Tx B ⊆ closure_of X Tx (A ∪ B).

An exact proof term for the current goal is (closure_monotone X Tx B (A ∪ B) Htop HBB_union HAB_sub).

Let x be given.

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

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

Assume HxA: x ∈ closure_of X Tx A.

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

Assume HxB: x ∈ closure_of X Tx B.

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

∎