∀ {α : Type u} {g : Set (Set α)} {motive : (a : Set α) → Filter.GenerateSets g a → Prop} {a : Set α}
  (t : Filter.GenerateSets g a),
  (∀ {s : Set α} (a : s ∈ g), motive s ⋯) →
    motive Set.univ ⋯ →
      (∀ {s t : Set α} (a : Filter.GenerateSets g s) (a_1 : s ⊆ t), motive t ⋯) →
        (∀ {s t : Set α} (a : Filter.GenerateSets g s) (a_1 : Filter.GenerateSets g t), motive (s ∩ t) ⋯) → motive a t