Let X, Tx, A and x be given.
Assume HTx: topology_on X Tx.
Assume HAsub: A ⊆ X.
Assume Hseq: ∃seq : set, sequence_in seq A ∧ converges_to X Tx seq x.
We will prove x ∈ closure_of X Tx A.
Apply Hseq to the current goal.
Let seq be given.
Assume Hseqpair.
We prove the intermediate claim Hseqin: sequence_in seq A.
An exact proof term for the current goal is (andEL (sequence_in seq A) (converges_to X Tx seq x) Hseqpair).
We prove the intermediate claim Hconv: converges_to X Tx seq x.
An exact proof term for the current goal is (andER (sequence_in seq A) (converges_to X Tx seq x) Hseqpair).
We prove the intermediate claim HxX: x ∈ X.
We prove the intermediate claim Hleft: (topology_on X Tx ∧ sequence_on seq X) ∧ x ∈ X.
An exact proof term for the current goal is (andEL ((topology_on X Tx ∧ sequence_on seq X) ∧ x ∈ X) (∀U : set, U ∈ Tx → x ∈ U → ∃N : set, N ∈ ω ∧ ∀n : set, n ∈ ω → N ⊆ n → apply_fun seq n ∈ U) Hconv).
An exact proof term for the current goal is (andER (topology_on X Tx ∧ sequence_on seq X) (x ∈ X) Hleft).
We prove the intermediate claim Hcliff: x ∈ closure_of X Tx A ↔ (∀U ∈ Tx, x ∈ U → U ∩ A ≠ Empty).
An exact proof term for the current goal is (closure_characterization X Tx A x HTx HxX).
Apply (iffER (x ∈ closure_of X Tx A) (∀U ∈ Tx, x ∈ U → U ∩ A ≠ Empty) Hcliff) to the current goal.
We will prove ∀U ∈ Tx, x ∈ U → U ∩ A ≠ Empty.
Let U be given.
Assume HU: U ∈ Tx.
Assume HxU: x ∈ U.
We prove the intermediate claim Hevent: ∃N : set, N ∈ ω ∧ ∀n : set, n ∈ ω → N ⊆ n → apply_fun seq n ∈ U.
We prove the intermediate claim Htail0: ∀V : set, V ∈ Tx → x ∈ V → ∃N : set, N ∈ ω ∧ ∀n : set, n ∈ ω → N ⊆ n → apply_fun seq n ∈ V.
An exact proof term for the current goal is (andER ((topology_on X Tx ∧ sequence_on seq X) ∧ x ∈ X) (∀V : set, V ∈ Tx → x ∈ V → ∃N : set, N ∈ ω ∧ ∀n : set, n ∈ ω → N ⊆ n → apply_fun seq n ∈ V) Hconv).
An exact proof term for the current goal is (Htail0 U HU HxU).
Apply Hevent to the current goal.
Let N be given.
Assume HNpair.
We prove the intermediate claim HNomega: N ∈ ω.
An exact proof term for the current goal is (andEL (N ∈ ω) (∀n : set, n ∈ ω → N ⊆ n → apply_fun seq n ∈ U) HNpair).
We prove the intermediate claim Htail: ∀n : set, n ∈ ω → N ⊆ n → apply_fun seq n ∈ U.
An exact proof term for the current goal is (andER (N ∈ ω) (∀n : set, n ∈ ω → N ⊆ n → apply_fun seq n ∈ U) HNpair).
We prove the intermediate claim HyU: apply_fun seq N ∈ U.
An exact proof term for the current goal is (Htail N HNomega (Subq_ref N)).
We prove the intermediate claim HyA: apply_fun seq N ∈ A.
An exact proof term for the current goal is (Hseqin N HNomega).
We will prove U ∩ A ≠ Empty.
Assume HUAEq: U ∩ A = Empty.
We prove the intermediate claim HyUA: apply_fun seq N ∈ U ∩ A.
An exact proof term for the current goal is (binintersectI U A (apply_fun seq N) HyU HyA).
We prove the intermediate claim HyEmp: apply_fun seq N ∈ Empty.
rewrite the current goal using HUAEq (from right to left).
An exact proof term for the current goal is HyUA.
An exact proof term for the current goal is (EmptyE (apply_fun seq N) HyEmp False).
∎