Let X and S be given.
Assume HS.
We will prove topology_on X (generated_topology_from_subbasis X S).
We prove the intermediate claim HBasis: basis_on X (basis_of_subbasis X S).
An exact proof term for the current goal is (finite_intersections_basis_of_subbasis X S HS).
We prove the intermediate claim HTopo: topology_on X (generated_topology X (basis_of_subbasis X S)).
An exact proof term for the current goal is (lemma_topology_from_basis X (basis_of_subbasis X S) HBasis).
An exact proof term for the current goal is HTopo.
∎