∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {p : Ideal S},
  Algebra.ZariskisMainProperty R p ↔
    ∃ r ∉ p, ∃ (h : IsIntegral R r), (integralClosure R S).saturation (Submonoid.powers r) ⋯ = ⊤