{α : Type u_1} →
  (E : Set α) →
    (Indep : Set α → Prop) →
      Indep ∅ →
        (∀ ⦃I J : Set α⦄, Indep J → I ⊆ J → Indep I) →
          (∀ ⦃I B : Set α⦄, Indep I → ¬Maximal Indep I → Maximal Indep B → ∃ x ∈ B \ I, Indep (insert x I)) →
            (∀ (I : Set α), (∀ J ⊆ I, J.Finite → Indep J) → Indep I) → (∀ (I : Set α), Indep I → I ⊆ E) → IndepMatroid α