∀ {α : Type u_2} {M : Matroid α} {I : Set α} {ι : Type u_4},
  M.Indep I →
    ∀ {X : ι → Set α} {A : Set ι},
      A.Nonempty → (∀ i ∈ A, M.IsBasis (X i ∩ I) (X i)) → M.IsBasis ((⋂ i ∈ A, X i) ∩ I) (⋂ i ∈ A, X i)