∀ {R : Type u_1} [inst : CommSemiring R] (S : Type u_2) [inst_1 : CommSemiring S] [inst_2 : Algebra R S] (I : Ideal R)
  [hI : I.IsPrime] [inst_3 : IsLocalization.AtPrime S I] (a : { p // p.IsPrime ∧ p ≤ I }),
  ↑↑((RelIso.symm (IsLocalization.AtPrime.orderIsoOfPrime S I)) a) =
    ⋂ s,
      ⋂ (_ :
        ↑↑((OrderIso.setCongr (fun p => p.IsPrime ∧ Disjoint ↑I.primeCompl ↑p) (fun p => p.IsPrime ∧ p ≤ I) ⋯).symm a) ⊆
          ⇑(algebraMap R S) ⁻¹' ↑s),
        ↑s