∀ {α : Type u_1} {S : Set (Set α)} {motive : (a : Set α) → generatePiSystem S a → Prop}
  {motive_1 : {a : Set α} → (t : generatePiSystem S a) → generatePiSystem.below t → Prop} {a : Set α}
  {t : generatePiSystem S a} (t_1 : generatePiSystem.below t),
  (∀ {s : Set α} (h_s : s ∈ S), motive_1 ⋯ ⋯) →
    (∀ {s t : Set α} (h_s : generatePiSystem S s) (h_t : generatePiSystem S t) (h_nonempty : (s ∩ t).Nonempty)
        (ih : generatePiSystem.below h_s) (h_s_ih : motive s h_s) (ih_1 : generatePiSystem.below h_t)
        (h_t_ih : motive t h_t), motive_1 ⋯ ⋯) →
      motive_1 t t_1