Let X and S be given.

Assume HS: countable_set S.

We will prove countable_set (finite_intersections_of X S).

Set FS to be the term finite_subcollections S.

We prove the intermediate claim HFS: countable_set FS.

An exact proof term for the current goal is (finite_subcollections_countable S HS).

An exact proof term for the current goal is (countable_image FS HFS (λF0 : set ⇒ intersection_of_family X F0)).

∎