∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] {X : C} (a b : CategoryTheory.Sieve X),
  (fun S R => ∀ ⦃Y : C⦄ (f : Y ⟶ X), S.arrows f → R.arrows f) a b ∧
      ¬(fun S R => ∀ ⦃Y : C⦄ (f : Y ⟶ X), S.arrows f → R.arrows f) b a ↔
    (∀ ⦃Y : C⦄ (f : Y ⟶ X), a.arrows f → b.arrows f) ∧ ¬∀ ⦃Y : C⦄ (f : Y ⟶ X), b.arrows f → a.arrows f