rw [<-Set.union_inter_distrib_right]
α : Type u_1
A✝ B✝ I J X : Set α
M✝ : RankMatroid α
x : α
M : RankMatroid α
A B : Set α
h : ∀ {A B : Set α}, A ⊆ B → B ⊆ M.E → M.relRank A B = M.matroid.relRank A B
A' : Set α := A ∩ M.E
B' : Set α := B ∩ M.E ∪ A'
⊢ B ∩ M.E ∪ A ∩ M.E ⊆ M.E
α : Type u_1
A✝ B✝ I J X : Set α
M✝ : RankMatroid α
x : α
M : RankMatroid α
A B : Set α
h : ∀ {A B : Set α}, A ⊆ B → B ⊆ M.E → M.relRank A B = M.matroid.relRank A B
A' : Set α := A ∩ M.E
B' : Set α := B ∩ M.E ∪ A'
⊢ (B ∪ A) ∩ M.E ⊆ M.E