Let X, Tx and Fam be given.
Assume HTx: topology_on X Tx.
Assume Hcov: open_cover X Tx Fam.
We will prove open_cover_of X Tx Fam.
We will prove topology_on X Tx ∧ Fam ⊆ 𝒫 X ∧ X ⊆ ⋃ Fam ∧ (∀U : set, U ∈ Fam → U ∈ Tx).
Apply and4I to the current goal.
An exact proof term for the current goal is HTx.
An exact proof term for the current goal is (open_cover_family_sub X Tx Fam HTx Hcov).
We prove the intermediate claim Hcovers: covers X Fam.
An exact proof term for the current goal is (andER (∀u0 : set, u0 ∈ Fam → u0 ∈ Tx) (covers X Fam) Hcov).
An exact proof term for the current goal is (covers_implies_Subq_Union X Fam Hcovers).
Let U be given.
Assume HU: U ∈ Fam.
We prove the intermediate claim Hopens: ∀u0 : set, u0 ∈ Fam → u0 ∈ Tx.
An exact proof term for the current goal is (andEL (∀u0 : set, u0 ∈ Fam → u0 ∈ Tx) (covers X Fam) Hcov).
An exact proof term for the current goal is (Hopens U HU).
∎