∀ {α : Type u_1} [inst : MeasurableSpace α] {s : MeasureTheory.SignedMeasure α} {i : Set α},
  MeasurableSet i →
    ↑s i < 0 →
      (¬∀ (n : ℕ),
            ¬MeasureTheory.VectorMeasure.restrict s
                  (i \ ⋃ l, ⋃ (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq✝ s i l) ≤
                MeasureTheory.VectorMeasure.restrict 0
                  (i \ ⋃ l, ⋃ (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq✝¹ s i l)) →
        ∃ j,
          MeasurableSet j ∧
            j ⊆ i ∧ MeasureTheory.VectorMeasure.restrict s j ≤ MeasureTheory.VectorMeasure.restrict 0 j ∧ ↑s j < 0