∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W₁ W₂ : CategoryTheory.MorphismProperty C},
  W₁.rlp = W₂ →
    W₂.llp = W₁ →
      autoParam (W₁.HasFactorization W₂)
          CategoryTheory.MorphismProperty.IsWeakFactorizationSystem.hasFactorization._autoParam →
        W₁.IsWeakFactorizationSystem W₂