exact union_subset (diff_subset.trans hX) (diff_subset.trans diff_subset)
α : Type u_1
M✝ : Matroid α
B B' I I' J K X✝¹ Y : Set α
M : Matroid α
X✝ X : Set α
hX : X ⊆ M.E
BX : Set α
hBXb : M.Base BX
hI : M.Basis (BX ∩ X) X
hIBX : BX ∩ X ⊆ BX
hBXdual : M✶.Basis ((M.E \ X) \ BX) (M.E \ X)
BY : Set α
hBYb : M.Base BY
hJ : M.Basis (BY ∩ (M.E \ X)) (M.E \ X)
hBX : M.Basis BX (BX ∩ X ∪ BY ∩ (M.E \ X))
hIJE : M.Spanning (BX ∩ X ∪ BY ∩ (M.E \ X))
hBY : M.Basis BY (BX ∩ X ∪ BY ∩ (M.E \ X))
hJBY : BY ∩ (M.E \ X) ⊆ BY
hBYdual : M✶.Basis (X \ BY) X
⊢ X \ BY ∪ (M.E \ X) \ BX ⊆ M✶.E
no goals