An exact proof term for the current goal is (lemma_topology_from_basis R R_lower_limit_basis R_lower_limit_basis_is_basis_local).