We will prove topology_on R R_standard_topology.

An exact proof term for the current goal is (lemma_topology_from_basis R R_standard_basis (R_standard_basis_is_basis)).

∎