∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] {X : C} (Y : CategoryTheory.Subobject X)
  (Z : CategoryTheory.Subobject (CategoryTheory.Subobject.underlying.obj Y)),
  CategoryTheory.Subobject.mk (CategoryTheory.CategoryStruct.comp Z.arrow Y.arrow) ∈ Set.Iic Y