exact mem_of_mem_of_subset heX.1 (cl_subset_cl _ diff_subset)
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e f x : α
I C : Set α
he : M.Nonloop e
hf : f ∉ M.E
X : Set α
heX : f ∈ (M.parallelExtend e f).cl (X \ {f}) ∧ e ∉ {f}
⊢ f ∈ (M.parallelExtend e f).cl X
no goals