∀ {C : Type u₁} [inst : CategoryTheory.Category.{v, u₁} C] (X : C),
  CategoryTheory.EssentiallySmall.{w, v, max u₁ v} (CategoryTheory.MonoOver X) ↔
    Small.{w, max u₁ v} (CategoryTheory.Subobject X)