Let X, Tx and Fam be given.
Assume H: open_cover_of X Tx Fam.
We prove the intermediate claim H0: ((topology_on X Tx ∧ Fam ⊆ 𝒫 X) ∧ X ⊆ ⋃ Fam) ∧ (∀U : set, U ∈ Fam → U ∈ Tx).
An exact proof term for the current goal is H.
We prove the intermediate claim H1: (topology_on X Tx ∧ Fam ⊆ 𝒫 X) ∧ X ⊆ ⋃ Fam.
An exact proof term for the current goal is (andEL ((topology_on X Tx ∧ Fam ⊆ 𝒫 X) ∧ X ⊆ ⋃ Fam) (∀U : set, U ∈ Fam → U ∈ Tx) H0).
We prove the intermediate claim H2: topology_on X Tx ∧ Fam ⊆ 𝒫 X.
An exact proof term for the current goal is (andEL (topology_on X Tx ∧ Fam ⊆ 𝒫 X) (X ⊆ ⋃ Fam) H1).
An exact proof term for the current goal is (andER (topology_on X Tx) (Fam ⊆ 𝒫 X) H2).
∎