∀ {R : Type u_1} [inst : CommSemiring R] {S : Type u_2} [inst_1 : CommRing S] [inst_2 : Algebra R S] {I p : Ideal R}
  {P : Ideal S} [P.IsPrime] [P.LiesOver p],
  p ∈ I.minimalPrimes →
    ∀ {J : Ideal S},
      J ≤ P →
        Ideal.map (Ideal.Quotient.mk (Ideal.map (algebraMap R S) p)) P ∈
            (Ideal.map (Ideal.Quotient.mk (Ideal.map (algebraMap R S) p)) J).minimalPrimes →
          P ∈ (Ideal.map (algebraMap R S) I ⊔ J).minimalPrimes