Let X, Tx and Fam be given.

Assume H: open_cover_of X Tx Fam.

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

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

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

∎