Let X, B and U be given.
Assume HUpow: U ∈ 𝒫 X.
Assume HUinB: U ∈ B.
We will prove U ∈ generated_topology X B.
We prove the intermediate claim HUprop: ∀x ∈ U, ∃b ∈ B, x ∈ b ∧ b ⊆ U.
Let x be given.
Assume HxU: x ∈ U.
We use U to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HUinB.
Apply andI to the current goal.
An exact proof term for the current goal is HxU.
An exact proof term for the current goal is (Subq_ref U).
An exact proof term for the current goal is (SepI (𝒫 X) (λU0 : set ⇒ ∀x ∈ U0, ∃b ∈ B, x ∈ b ∧ b ⊆ U0) U HUpow HUprop).
∎