Let X and Tx be given.
Assume HB: Baire_space X Tx.
Let U be given.
Assume HUsub: U ⊆ Tx.
Assume HUcount: countable_set U.
Assume HUdense: ∀u : set, u ∈ U → u ∈ Tx ∧ dense_in u X Tx.
We will prove dense_in (intersection_over_family X U) X Tx.
We prove the intermediate claim Hprop: ∀U0 : set, U0 ⊆ Tx → countable_set U0 → (∀u : set, u ∈ U0 → u ∈ Tx ∧ dense_in u X Tx) → dense_in (intersection_over_family X U0) X Tx.
An exact proof term for the current goal is (andER (topology_on X Tx) (∀U0 : set, U0 ⊆ Tx → countable_set U0 → (∀u : set, u ∈ U0 → u ∈ Tx ∧ dense_in u X Tx) → dense_in (intersection_over_family X U0) X Tx) HB).
An exact proof term for the current goal is (Hprop U HUsub HUcount HUdense).
∎