Let X, Tx and A be given.
Assume Htop: topology_on X Tx.
Assume HA: A ⊆ X.
We will prove closure_of X Tx (closure_of X Tx A) = closure_of X Tx A.
We prove the intermediate claim HclA_sub: closure_of X Tx A ⊆ X.
An exact proof term for the current goal is (closure_in_space X Tx A Htop).
Apply set_ext to the current goal.
We prove the intermediate claim HclA_closed: closed_in X Tx (closure_of X Tx A).
An exact proof term for the current goal is (closure_is_closed X Tx A Htop HA).
We prove the intermediate claim Heq: closure_of X Tx (closure_of X Tx A) = closure_of X Tx A.
An exact proof term for the current goal is (closed_closure_eq X Tx (closure_of X Tx A) Htop HclA_closed).
Let x be given.
Assume Hx: x ∈ closure_of X Tx (closure_of X Tx A).
rewrite the current goal using Heq (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 (closure_of X Tx A) Htop HclA_sub).
∎