Let X, Tx and Fam be given.
Assume HTx: topology_on X Tx.
Assume HFsubX: ∀A : set, A ∈ Fam → A ⊆ X.
Assume HLF: locally_finite_family X Tx Fam.
Let x be given.
Assume HxX: x ∈ X.
Set ClFam to be the term {closure_of X Tx A|A ∈ Fam}.
We prove the intermediate claim HLFcl: locally_finite_family X Tx ClFam.
An exact proof term for the current goal is (lemma39_1b_closures_locally_finite X Tx Fam HFsubX HLF).
We prove the intermediate claim HexS: ∃S : set, finite S ∧ S ⊆ ClFam ∧ ∀B : set, B ∈ ClFam → x ∈ B → B ∈ S.
An exact proof term for the current goal is (locally_finite_family_point_finite_ex X Tx ClFam HLFcl x HxX).
Apply HexS to the current goal.
Let S be given.
Assume HS: finite S ∧ S ⊆ ClFam ∧ ∀B : set, B ∈ ClFam → x ∈ B → B ∈ S.
We use S to witness the existential quantifier.
Apply andI to the current goal.
We prove the intermediate claim HS1: finite S ∧ S ⊆ ClFam.
An exact proof term for the current goal is (andEL (finite S ∧ S ⊆ ClFam) (∀B : set, B ∈ ClFam → x ∈ B → B ∈ S) HS).
An exact proof term for the current goal is HS1.
We prove the intermediate claim HSprop: ∀B : set, B ∈ ClFam → x ∈ B → B ∈ S.
An exact proof term for the current goal is (andER (finite S ∧ S ⊆ ClFam) (∀B : set, B ∈ ClFam → x ∈ B → B ∈ S) HS).
Let A be given.
Assume HA: A ∈ Fam.
Assume Hxcl: x ∈ closure_of X Tx A.
We prove the intermediate claim HclIn: closure_of X Tx A ∈ ClFam.
An exact proof term for the current goal is (ReplI Fam (λA0 : set ⇒ closure_of X Tx A0) A HA).
An exact proof term for the current goal is (HSprop (closure_of X Tx A) HclIn Hxcl).
∎