Let Fam be given.

Assume HFamEmpty: ∀T : set, T ∈ Fam → Empty ∈ T.

Let X be given.

We will prove Empty ∈ Intersection_Fam X Fam.

We prove the intermediate claim HEmptyPower: Empty ∈ 𝒫 X.

Apply PowerI to the current goal.

Apply Subq_Empty to the current goal.

An exact proof term for the current goal is (SepI (𝒫 X) (λU ⇒ ∀T : set, T ∈ Fam → U ∈ T) Empty HEmptyPower HFamEmpty).

∎