refine subset_antisymm ?_ (h₁.flat_right.cl_subset_of_subset (union_subset h₀.subset h₁.subset))
α : Type u_1
M : Matroid α
I F X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e f : α
h₀ : F₀ ⋖[M] F
h₁ : F₁ ⋖[M] F
hne : F₀ ≠ F₁
⊢ F = M.cl (F₀ ∪ F₁)
α : Type u_1
M : Matroid α
I F X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e f : α
h₀ : F₀ ⋖[M] F
h₁ : F₁ ⋖[M] F
hne : F₀ ≠ F₁
⊢ F ⊆ M.cl (F₀ ∪ F₁)