Let Xi, Ti, i and A be given.
Assume Hchain: coherent_chain Xi Ti.
Assume HiO: i ∈ ω.
Assume HAcl: closed_in (apply_fun Xi i) (apply_fun Ti i) A.
Set Xi_i to be the term apply_fun Xi i.
Set Ti_i to be the term apply_fun Ti i.
Set Xi_s to be the term apply_fun Xi (ordsucc i).
Set Ti_s to be the term apply_fun Ti (ordsucc i).
Set A0 to be the term (∀j : set, j ∈ ω → topology_on (apply_fun Xi j) (apply_fun Ti j)).
Set B0 to be the term (∀j : set, j ∈ ω → apply_fun Xi j ⊆ apply_fun Xi (ordsucc j)).
Set C0 to be the term (∀j : set, j ∈ ω → subspace_topology (apply_fun Xi (ordsucc j)) (apply_fun Ti (ordsucc j)) (apply_fun Xi j) = apply_fun Ti j).
Set D0 to be the term (∀j : set, j ∈ ω → closed_in (apply_fun Xi (ordsucc j)) (apply_fun Ti (ordsucc j)) (apply_fun Xi j)).
We prove the intermediate claim Habc: (A0 ∧ B0) ∧ C0.
An exact proof term for the current goal is (andEL ((A0 ∧ B0) ∧ C0) D0 Hchain).
We prove the intermediate claim HD: D0.
An exact proof term for the current goal is (andER ((A0 ∧ B0) ∧ C0) D0 Hchain).
We prove the intermediate claim Hab: A0 ∧ B0.
An exact proof term for the current goal is (andEL (A0 ∧ B0) C0 Habc).
We prove the intermediate claim HC: C0.
An exact proof term for the current goal is (andER (A0 ∧ B0) C0 Habc).
We prove the intermediate claim HA: A0.
An exact proof term for the current goal is (andEL A0 B0 Hab).
We prove the intermediate claim Hsubeq: subspace_topology Xi_s Ti_s Xi_i = Ti_i.
An exact proof term for the current goal is (HC i HiO).
We prove the intermediate claim HXi_i_closed: closed_in Xi_s Ti_s Xi_i.
An exact proof term for the current goal is (HD i HiO).
We prove the intermediate claim HTs: topology_on Xi_s Ti_s.
An exact proof term for the current goal is (HA (ordsucc i) (omega_ordsucc i HiO)).
We will prove closed_in Xi_s Ti_s A.
Apply (closed_in_closed_subspace Xi_s Ti_s Xi_i A HTs HXi_i_closed) to the current goal.
rewrite the current goal using Hsubeq (from left to right).
An exact proof term for the current goal is HAcl.
∎