∀ {α : Type u_1} {S : Set (Set α)} {motive : (a : Set α) → generatePiSystem S a → Prop},
  (∀ {s : Set α} (h_s : s ∈ S), motive s ⋯) →
    (∀ {s t : Set α} (h_s : generatePiSystem S s) (h_t : generatePiSystem S t) (h_nonempty : (s ∩ t).Nonempty),
        motive s h_s → motive t h_t → motive (s ∩ t) ⋯) →
      ∀ {a : Set α} (t : generatePiSystem S a), motive a t