Let X, Tx and Fam be given.

Assume Hof: open_cover_of X Tx Fam.

We will prove open_cover X Tx Fam.

We will prove (∀u : set, u ∈ Fam → u ∈ Tx) ∧ covers X Fam.

Apply andI to the current goal.

Let u be given.

Assume HuFam: u ∈ Fam.

An exact proof term for the current goal is (open_cover_of_members_open X Tx Fam u Hof HuFam).

We prove the intermediate claim Hsub: X ⊆ ⋃ Fam.

An exact proof term for the current goal is (open_cover_of_covers X Tx Fam Hof).

An exact proof term for the current goal is (Subq_Union_implies_covers X Fam Hsub).

∎