∀ {α : Type u_1} {M : Matroid α} {I X : Set α},
  M.Indep I →
    I ⊆ X →
      (∀ ⦃J : Set α⦄, M.Indep J → I ⊆ J → J ⊆ X → J ⊆ I) →
        autoParam (X ⊆ M.E) Matroid.Indep.isBasis_of_maximal_subset._auto_1 → M.IsBasis I X