An exact proof term for the current goal is (lemma_topology_from_basis R R_upper_limit_basis R_upper_limit_basis_is_basis_local).