Let X, Tx, Fam and U be given.

Assume H: open_cover_of X Tx Fam.

Assume HU: U ∈ Fam.

We prove the intermediate claim HTx: topology_on X Tx.

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

We prove the intermediate claim HUin: U ∈ Tx.

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

An exact proof term for the current goal is (open_inI X Tx U HTx HUin).

∎