rintro hCD
case mp.intro.intro.intro.intro.intro.intro
α : Type u_1
M M' : Matroid α
e f : α
I J R B X Y Z K : Set α
M₀ M₁ M₂ : Matroid α
C D : Set α
hC : C ⊆ M.E
hD : D ⊆ M.E
hCD : Disjoint C D
hss : (M ／ C ＼ D).E ⊂ M.E
⊢ C ∪ D ≠ ∅
case mp.intro.intro.intro.intro.intro.intro
α : Type u_1
M M' : Matroid α
e f : α
I J R B X Y Z K : Set α
M₀ M₁ M₂ : Matroid α
C D : Set α
hC : C ⊆ M.E
hD : D ⊆ M.E
hCD✝ : Disjoint C D
hss : (M ／ C ＼ D).E ⊂ M.E
hCD : C ∪ D = ∅
⊢ False