∀ {d b : ℝ},
  d ≤ b →
    ∀ {u : Set (ℝ × ℝ)},
      (∀ (s : Finset ↑u) (i : ℕ), d ≤ (((fun s => Finset.image Subtype.val s) s).intervalGapsWithin ⋯ d b ↑i).1) →
        (∀ (s : Finset ↑u) (i : ℕ),
            (((fun s => Finset.image Subtype.val s) s).intervalGapsWithin ⋯ d b ↑i).1 ≤
              (((fun s => Finset.image Subtype.val s) s).intervalGapsWithin ⋯ d b ↑i).2) →
          (∀ (s : Finset ↑u) (i : ℕ), (((fun s => Finset.image Subtype.val s) s).intervalGapsWithin ⋯ d b ↑i).2 ≤ b) →
            (∀ (s : Finset ↑u),
                (Set.Iio (((fun s => Finset.image Subtype.val s) s).card + 1)).PairwiseDisjoint fun j =>
                  Set.Ioc (((fun s => Finset.image Subtype.val s) s).intervalGapsWithin ⋯ d b ↑j).1
                    (((fun s => Finset.image Subtype.val s) s).intervalGapsWithin ⋯ d b ↑j).2) →
              ∀ ⦃s : Finset ↑u⦄,
                (fun s =>
                      (((fun s => Finset.image Subtype.val s) s).card + 1, fun i =>
                        ((fun s => Finset.image Subtype.val s) s).intervalGapsWithin ⋯ d b ↑i))
                    s ∈
                  AbsolutelyContinuousOnInterval.disjWithin d b