exact h.1.2 M.ground_spanning
α : Type u_1
M : Matroid α
I F X Y F' F₀ F₁ F₂ P L H₁ H₂ H' B C K : Set α
e f : α
h : (M.E ⊆ M.E ∧ ¬M.Spanning M.E) ∧ ∀ ⦃y : Set α⦄, y ⊆ M.E → ¬M.Spanning y → M.E ⊆ y → M.E = y
⊢ False
no goals