∀ {α : Type u_1} (Indep : Set α → Prop),
  (∀ ⦃I J : Set α⦄, Indep J → I ⊆ J → Indep I) →
    (∀ ⦃I J : Set α⦄, Indep I → Indep J → I.encard < J.encard → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I)) →
      (∃ n, ∀ (I : Set α), Indep I → I.encard ≤ ↑n) →
        ∀ ⦃I B : Set α⦄, Indep I → ¬Maximal Indep I → Maximal Indep B → ∃ x ∈ B \ I, Indep (insert x I)