Let X, B and U be given.
Assume HU: U ∈ generated_topology X B.
We will prove U ⊆ X.
We prove the intermediate claim HUPower: U ∈ 𝒫 X.
An exact proof term for the current goal is (SepE1 (𝒫 X) (λU0 ⇒ ∀x ∈ U0, ∃b ∈ B, x ∈ b ∧ b ⊆ U0) U HU).
An exact proof term for the current goal is (PowerE X U HUPower).
∎