∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {κ : Cardinal.{w}} [inst_1 : Fact κ.IsRegular]
  [CategoryTheory.LocallySmall.{w, v, u} C],
  ∀ P ≤ CategoryTheory.isCardinalPresentable C κ, P.colimitsCardinalClosure κ ≤ CategoryTheory.isCardinalPresentable C κ