∀ {α : Type u} {g : Set (Set α)} {motive : (a : Set α) → Filter.GenerateSets g a → Prop}
  {motive_1 : {a : Set α} → (t : Filter.GenerateSets g a) → Filter.GenerateSets.below t → Prop},
  (∀ {s : Set α} (a : s ∈ g), motive_1 ⋯ ⋯) →
    motive_1 ⋯ ⋯ →
      (∀ {s t : Set α} (a : Filter.GenerateSets g s) (a_1 : s ⊆ t) (ih : Filter.GenerateSets.below a)
          (a_ih : motive s a), motive_1 a ih → motive_1 ⋯ ⋯) →
        (∀ {s t : Set α} (a : Filter.GenerateSets g s) (a_1 : Filter.GenerateSets g t)
            (ih : Filter.GenerateSets.below a) (a_ih : motive s a) (ih_1 : Filter.GenerateSets.below a_1)
            (a_ih_1 : motive t a_1), motive_1 a ih → motive_1 a_1 ih_1 → motive_1 ⋯ ⋯) →
          ∀ {a : Set α} {t : Filter.GenerateSets g a} (t_1 : Filter.GenerateSets.below t), motive_1 t t_1