Let X, B and B' be given.
Assume HBasis Href.
We prove the intermediate claim Hprop: ∀U ∈ generated_topology X B, ∀x ∈ U, ∃b' ∈ B', x ∈ b' ∧ b' ⊆ U.
An exact proof term for the current goal is (andER (topology_on X (generated_topology X B)) (∀U ∈ generated_topology X B, ∀x ∈ U, ∃b' ∈ B', x ∈ b' ∧ b' ⊆ U) Href).
We will prove generated_topology X B ⊆ generated_topology X B'.
Let U be given.
Assume HU.
We prove the intermediate claim HUsubX: U ⊆ X.
An exact proof term for the current goal is (PowerE X U (SepE1 (𝒫 X) (λU0 : set ⇒ ∀x0 ∈ U0, ∃b0 ∈ B, x0 ∈ b0 ∧ b0 ⊆ U0) U HU)).
We prove the intermediate claim HUprop: ∀x ∈ U, ∃b' ∈ B', x ∈ b' ∧ b' ⊆ U.
An exact proof term for the current goal is (Hprop U HU).
An exact proof term for the current goal is (SepI (𝒫 X) (λU0 : set ⇒ ∀x0 ∈ U0, ∃b0 ∈ B', x0 ∈ b0 ∧ b0 ⊆ U0) U (PowerI X U HUsubX) HUprop).
∎