Let X, S and s be given.
Assume HS HsS.
Apply (xm (s = Empty)) to the current goal.
Assume HsEmpty.
rewrite the current goal using HsEmpty (from left to right).
We prove the intermediate claim HT: topology_on X (generated_topology_from_subbasis X S).
An exact proof term for the current goal is (topology_from_subbasis_is_topology X S HS).
An exact proof term for the current goal is (topology_has_empty X (generated_topology_from_subbasis X S) HT).
Assume HsNe.
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 HsBasis: s ∈ basis_of_subbasis X S.
An exact proof term for the current goal is (subbasis_elem_in_basis X S s HS HsS HsNe).
An exact proof term for the current goal is (generated_topology_contains_basis X (basis_of_subbasis X S) HBasis s HsBasis).
∎