Let X, Tx, C and D be given.
Assume Htop: topology_on X Tx.
Assume HC: closed_in X Tx C.
Assume HD: closed_in X Tx D.
We will prove closure_of X Tx (C ∪ D) = C ∪ D.
We prove the intermediate claim HCD_closed: closed_in X Tx (C ∪ D).
An exact proof term for the current goal is (union_of_closed_is_closed X Tx C D Htop HC HD).
We prove the intermediate claim HCD_sub: C ∪ D ⊆ X.
Let x be given.
Assume Hx: x ∈ C ∪ D.
Apply (binunionE C D x Hx) to the current goal.
Assume HxC: x ∈ C.
We prove the intermediate claim HC_sub: C ⊆ X.
An exact proof term for the current goal is (andEL (C ⊆ X) (∃U ∈ Tx, C = X ∖ U) (andER (topology_on X Tx) (C ⊆ X ∧ ∃U ∈ Tx, C = X ∖ U) HC)).
An exact proof term for the current goal is (HC_sub x HxC).
Assume HxD: x ∈ D.
We prove the intermediate claim HD_sub: D ⊆ X.
An exact proof term for the current goal is (andEL (D ⊆ X) (∃V ∈ Tx, D = X ∖ V) (andER (topology_on X Tx) (D ⊆ X ∧ ∃V ∈ Tx, D = X ∖ V) HD)).
An exact proof term for the current goal is (HD_sub x HxD).
Apply set_ext to the current goal.
Let x be given.
Assume Hx: x ∈ closure_of X Tx (C ∪ D).
We will prove x ∈ C ∪ D.
rewrite the current goal using (closed_closure_eq X Tx (C ∪ D) Htop HCD_closed) (from right to left).
An exact proof term for the current goal is Hx.
An exact proof term for the current goal is (subset_of_closure X Tx (C ∪ D) Htop HCD_sub).
∎