rw [modularSet_iff]
ι : Type u_1
α : Type u_2
M✝ : Matroid α
B I J X✝ X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e f : α
M : Matroid α
X : Set α
⊢ M.ModularSet X ↔ ∀ ⦃F : Set α⦄, M.Flat F → ∃ I, M.Indep I ∧ X ⊆ M.cl (X ∩ I) ∧ F ⊆ M.cl (F ∩ I)
ι : Type u_1
α : Type u_2
M✝ : Matroid α
B I J X✝ X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e f : α
M : Matroid α
X : Set α
⊢ (∀ ⦃F : Set α⦄, M.Flat F → ∃ I, M.Indep I ∧ M.Basis (X ∩ I) X ∧ M.Basis (F ∩ I) F) ↔
    ∀ ⦃F : Set α⦄, M.Flat F → ∃ I, M.Indep I ∧ X ⊆ M.cl (X ∩ I) ∧ F ⊆ M.cl (F ∩ I)