Let X, Tx and Fam be given.
Assume HTx: topology_on X Tx.
Assume HFamSub: Fam ⊆ 𝒫 X.
Assume Hcov: X ⊆ ⋃ Fam.
Assume Hmem: ∀U : set, U ∈ Fam → U ∈ Tx.
We will prove open_cover_of X Tx Fam.
We prove the intermediate claim Hcore: ((topology_on X Tx ∧ Fam ⊆ 𝒫 X) ∧ X ⊆ ⋃ Fam) ∧ (∀U : set, U ∈ Fam → U ∈ Tx).
Apply andI to the current goal.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is HTx.
An exact proof term for the current goal is HFamSub.
An exact proof term for the current goal is Hcov.
An exact proof term for the current goal is Hmem.
An exact proof term for the current goal is Hcore.
∎