ext e
α : Type u_1
ι : Type u_2
M : Matroid α
F I✝ J X✝ Y B C R : Set α
e f x y : α
I E X : Set α
hb : (uniqueBaseOn (I ∩ E) E).Basis (X ∩ E ∩ (I ∩ E)) (X ∩ E)
⊢ (uniqueBaseOn I E).cl X = X ∩ I ∩ E ∪ E \ I
case h
α : Type u_1
ι : Type u_2
M : Matroid α
F I✝ J X✝ Y B C R : Set α
e✝ f x y : α
I E X : Set α
hb : (uniqueBaseOn (I ∩ E) E).Basis (X ∩ E ∩ (I ∩ E)) (X ∩ E)
e : α
⊢ e ∈ (uniqueBaseOn I E).cl X ↔ e ∈ X ∩ I ∩ E ∪ E \ I