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

We prove the intermediate claim HclA_closed: closed_in X Tx clA.

We prove the intermediate claim Hc: closure_of X Tx (closure_of X Tx A) = closure_of X Tx A ∧ closed_in X Tx (closure_of X Tx A).

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

An exact proof term for the current goal is (andER (closure_of X Tx (closure_of X Tx A) = closure_of X Tx A) (closed_in X Tx (closure_of X Tx A)) Hc).

We prove the intermediate claim HclB_closed: closed_in X Tx clB.

We prove the intermediate claim Hc: closure_of X Tx (closure_of X Tx B) = closure_of X Tx B ∧ closed_in X Tx (closure_of X Tx B).

An exact proof term for the current goal is (closure_idempotent_and_closed X Tx B Htop).

An exact proof term for the current goal is (andER (closure_of X Tx (closure_of X Tx B) = closure_of X Tx B) (closed_in X Tx (closure_of X Tx B)) Hc).

We prove the intermediate claim HclUnionClosed: closed_in X Tx (clA ∪ clB).

An exact proof term for the current goal is (union_of_closed_is_closed X Tx clA clB Htop HclA_closed HclB_closed).

We prove the intermediate claim HABsub: A ∪ B ⊆ clA ∪ clB.

Let y be given.

Assume Hy: y ∈ A ∪ B.

Apply (binunionE A B y Hy) to the current goal.

Assume HyA: y ∈ A.

We prove the intermediate claim HyclA: y ∈ clA.

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

An exact proof term for the current goal is (binunionI1 clA clB y HyclA).

Assume HyB: y ∈ B.

We prove the intermediate claim HyclB: y ∈ clB.

An exact proof term for the current goal is (subset_of_closure X Tx B Htop HB y HyB).

An exact proof term for the current goal is (binunionI2 clA clB y HyclB).

An exact proof term for the current goal is (closure_subset_of_closed_superset X Tx (A ∪ B) (clA ∪ clB) Htop HABsub HclUnionClosed).

Let x be given.

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

An exact proof term for the current goal is (Hsup x Hx).