Let X, S, U and x be given.
Assume HU: U ∈ generated_topology_from_subbasis X S.
Assume HxU: x ∈ U.
We will prove ∃b : set, b ∈ basis_of_subbasis X S ∧ x ∈ b ∧ b ⊆ U.
We prove the intermediate claim Hloc: ∀z ∈ U, ∃b ∈ basis_of_subbasis X S, z ∈ b ∧ b ⊆ U.
An exact proof term for the current goal is (SepE2 (𝒫 X) (λU0 : set ⇒ ∀z ∈ U0, ∃b ∈ basis_of_subbasis X S, z ∈ b ∧ b ⊆ U0) U HU).
We prove the intermediate claim Hexb: ∃b ∈ basis_of_subbasis X S, x ∈ b ∧ b ⊆ U.
An exact proof term for the current goal is (Hloc x HxU).
Apply Hexb to the current goal.
Let b be given.
Assume Hbprop.
We use b to witness the existential quantifier.
An exact proof term for the current goal is (and_assoc_rev (b ∈ basis_of_subbasis X S) (x ∈ b) (b ⊆ U) Hbprop).
∎