Let X, Tx and F be given.
Assume HTx: topology_on X Tx.
Assume HFfin: finite F.
Assume Hall: ∀C : set, C ∈ F → closed_in X Tx C.
Set p to be the term λF0 : set ⇒ (∀C : set, C ∈ F0 → closed_in X Tx C) → closed_in X Tx (⋃ F0).
We prove the intermediate claim HpEmpty: p Empty.
Assume Hall0: ∀C : set, C ∈ Empty → closed_in X Tx C.
rewrite the current goal using Union_Empty_eq (from left to right).
An exact proof term for the current goal is (Empty_is_closed X Tx HTx).
We prove the intermediate claim HpStep: ∀F0 y : set, finite F0 → y ∉ F0 → p F0 → p (F0 ∪ {y}).
Let F0 and y be given.
Assume HF0fin: finite F0.
Assume HyNot: y ∉ F0.
Assume IH: p F0.
Assume HallU: ∀C : set, C ∈ (F0 ∪ {y}) → closed_in X Tx C.
We prove the intermediate claim HallF0: ∀C : set, C ∈ F0 → closed_in X Tx C.
Let C be given.
Assume HC: C ∈ F0.
An exact proof term for the current goal is (HallU C (binunionI1 F0 {y} C HC)).
We prove the intermediate claim HUnionF0closed: closed_in X Tx (⋃ F0).
An exact proof term for the current goal is (IH HallF0).
We prove the intermediate claim HyClosed: closed_in X Tx y.
An exact proof term for the current goal is (HallU y (binunionI2 F0 {y} y (SingI y))).
rewrite the current goal using (Union_binunion_singleton_eq F0 y) (from left to right).
An exact proof term for the current goal is (closed_binunion X Tx (⋃ F0) y HUnionF0closed HyClosed).
We prove the intermediate claim HallF: p F.
An exact proof term for the current goal is (finite_ind p HpEmpty HpStep F HFfin).
An exact proof term for the current goal is (HallF Hall).
∎