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