Let X and S be given.
Assume HS: countable_set S.
We will prove countable_set (basis_of_subbasis X S).
We prove the intermediate claim Hfin: countable_set (finite_intersections_of X S).
An exact proof term for the current goal is (finite_intersections_of_countable X S HS).
We will prove countable (basis_of_subbasis X S).
Apply (Subq_countable (basis_of_subbasis X S) (finite_intersections_of X S)) to the current goal.
An exact proof term for the current goal is Hfin.
Let b be given.
Assume Hb: b ∈ basis_of_subbasis X S.
We will prove b ∈ finite_intersections_of X S.
An exact proof term for the current goal is (SepE1 (finite_intersections_of X S) (λb0 : set ⇒ b0 ≠ Empty) b Hb).
∎