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