exact fun hI ↦ ⟨fun h ↦ (M.cl_subset_ground _).antisymm h.2,
  fun h ↦ ⟨(M.subset_cl B).trans_eq h, h.symm.subset⟩⟩
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e f x y : α
⊢ M.Indep B → (B ⊆ M.E ∧ M.E ⊆ M.cl B ↔ M.cl B = M.E)
no goals