∀ {α : Type u_1} {s : ℕ → Set α} (n m : ℕ),
  s m ⊆ Set.dissipate s n →
    ∀ (k : ℕ),
      (fun x1 x2 => x1 ⊇ x2) (s m) (s k) ∧ (fun x1 x2 => x1 ⊇ x2) (s (n + 1)) (s k) →
        s k ⊆ Set.dissipate s n ∧ s k ⊆ s (n + 1)