rw [hE, ← diff_subset_iff] at hBE
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B✝ L L' I X Y Z F C K : Set α
hE : M.E = M.cl ∅ ∪ M✶.cl ∅
B : Set α
hBE : B ⊆ M.E
⊢ M.Base B ↔ B = M✶.cl ∅
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B✝ L L' I X Y Z F C K : Set α
hE : M.E = M.cl ∅ ∪ M✶.cl ∅
B : Set α
hBE : B \ M.cl ∅ ⊆ M✶.cl ∅
⊢ M.Base B ↔ B = M✶.cl ∅