Assume HAclosed: closed_in X Tx A.

We will prove limit_points_of X Tx A ⊆ A.

Let x be given.

Assume Hx: x ∈ limit_points_of X Tx A.

We will prove x ∈ A.

We prove the intermediate claim Heq_cl: closure_of X Tx A = A.

An exact proof term for the current goal is (closed_closure_eq X Tx A HTx HAclosed).

We prove the intermediate claim Heq_union: closure_of X Tx A = A ∪ limit_points_of X Tx A.

An exact proof term for the current goal is (closure_equals_set_plus_limit_points X Tx A HTx HA).

We prove the intermediate claim HxclA: x ∈ closure_of X Tx A.

rewrite the current goal using Heq_union (from left to right).

Apply binunionI2 to the current goal.

An exact proof term for the current goal is Hx.

We prove the intermediate claim HxA: x ∈ A.

rewrite the current goal using Heq_cl (from right to left).

An exact proof term for the current goal is HxclA.

An exact proof term for the current goal is HxA.

Assume Hlim_sub: limit_points_of X Tx A ⊆ A.

We will prove closed_in X Tx A.

We prove the intermediate claim Heq_union: closure_of X Tx A = A ∪ limit_points_of X Tx A.

An exact proof term for the current goal is (closure_equals_set_plus_limit_points X Tx A HTx HA).

We prove the intermediate claim Hunion_eq: A ∪ limit_points_of X Tx A = A.

Apply set_ext to the current goal.

Let x be given.

Assume Hx: x ∈ A ∪ limit_points_of X Tx A.

We will prove x ∈ A.

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

Assume HxA: x ∈ A.

An exact proof term for the current goal is HxA.

Assume Hxlim: x ∈ limit_points_of X Tx A.

An exact proof term for the current goal is (Hlim_sub x Hxlim).

Let x be given.

Assume HxA: x ∈ A.

We will prove x ∈ A ∪ limit_points_of X Tx A.

Apply binunionI1 to the current goal.

An exact proof term for the current goal is HxA.

We prove the intermediate claim HclA_eq: closure_of X Tx A = A.

rewrite the current goal using Heq_union (from left to right).

An exact proof term for the current goal is Hunion_eq.

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 HTx HA).

We will prove closed_in X Tx A.

rewrite the current goal using HclA_eq (from right to left).

An exact proof term for the current goal is HclA_closed.