Let X and Tx be given.
Assume Hsig: sigma_locally_finite_basis X Tx.
We prove the intermediate claim Hexists: ∃Fams : set, countable_set Fams ∧ Fams ⊆ 𝒫 (𝒫 X) ∧ (∀F : set, F ∈ Fams → locally_finite_family X Tx F) ∧ basis_generates X (⋃ Fams) Tx ∧ ∀b : set, b ∈ ⋃ Fams → b ∈ Tx.
An exact proof term for the current goal is (andER (topology_on X Tx) (∃Fams : set, countable_set Fams ∧ Fams ⊆ 𝒫 (𝒫 X) ∧ (∀F : set, F ∈ Fams → locally_finite_family X Tx F) ∧ basis_generates X (⋃ Fams) Tx ∧ ∀b : set, b ∈ ⋃ Fams → b ∈ Tx) Hsig).
An exact proof term for the current goal is Hexists.
∎