exact (hXY.symm.mono hJ.subset (hFI.trans hI.subset))
α : Type u_1
M : Matroid α
B B' I I' J K X Y F : Set α
hXY : Disjoint X Y
hI : M.Basis' I X
hJ : M.Basis' J Y
hFI : F ⊆ I
hF : M.Basis' (I \ F ∪ J) (X ∪ Y)
⊢ Disjoint J F
no goals