exact ⟨B, hB', hB.subset⟩
case intro
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X Y B✝ C R : Set α
e f x y : α
S T : Set α
h : M.Spanning S
B : Set α
hB : M.Basis B S
hB' : M.Base B
⊢ ∃ B, M.Base B ∧ B ⊆ S
no goals