Let x be given.

Assume HxU: x ∈ ⋃ Fam.

We will prove x ∈ X.

We prove the intermediate claim HsubFam: Fam ⊆ 𝒫 X.

An exact proof term for the current goal is (open_cover_of_family_sub X Tx Fam H).

Apply (UnionE Fam x HxU) to the current goal.

Let U be given.

Assume Hxpack: x ∈ U ∧ U ∈ Fam.

We prove the intermediate claim HxU0: x ∈ U.

An exact proof term for the current goal is (andEL (x ∈ U) (U ∈ Fam) Hxpack).

We prove the intermediate claim HUFam: U ∈ Fam.

An exact proof term for the current goal is (andER (x ∈ U) (U ∈ Fam) Hxpack).

We prove the intermediate claim HUPow: U ∈ 𝒫 X.

An exact proof term for the current goal is (HsubFam U HUFam).

We prove the intermediate claim HUsubX: U ⊆ X.

An exact proof term for the current goal is (PowerE X U HUPow).

An exact proof term for the current goal is (HUsubX x HxU0).