∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C],
  (∀ {X Y : C} (f : X ⟶ Y) [CategoryTheory.Mono f], Nonempty (CategoryTheory.NormalMono f)) →
    CategoryTheory.IsNormalMonoCategory C